Mathlib.Data.Int.Init

Int.le_rfl theorem

: a ≤ a

Full source

protected lemma le_rfl : a ≤ a := a.le_refl

Reflexivity of the Less-Than-or-Equal Relation on Integers

Informal description

For any integer $a$, it holds that $a \leq a$.

Int.lt_or_lt_of_ne theorem

: a ≠ b → a < b ∨ b < a

Full source

protected lemma lt_or_lt_of_ne : a ≠ b → a < b ∨ b < a := Int.lt_or_gt_of_ne

Trichotomy for Integers: $a \neq b$ implies $a < b$ or $b < a$

Informal description

For any integers $a$ and $b$, if $a \neq b$, then either $a < b$ or $b < a$.

Int.lt_or_le theorem

(a b : ℤ) : a < b ∨ b ≤ a

Full source

protected lemma lt_or_le (a b : ℤ) : a < b ∨ b ≤ a := by rw [← Int.not_lt]; exact Decidable.em _

Trichotomy Variant for Integers: $a < b$ or $b \leq a$

Informal description

For any integers $a$ and $b$, either $a$ is strictly less than $b$ or $b$ is less than or equal to $a$.

Int.le_or_lt theorem

(a b : ℤ) : a ≤ b ∨ b < a

Full source

protected lemma le_or_lt (a b : ℤ) : a ≤ b ∨ b < a := (b.lt_or_le a).symm

Trichotomy Variant for Integers: $a \leq b$ or $b < a$

Informal description

For any integers $a$ and $b$, either $a \leq b$ or $b < a$.

Int.lt_asymm theorem

: a < b → ¬b < a

Full source

protected lemma lt_asymm : a < b → ¬ b < a := by rw [Int.not_lt]; exact Int.le_of_lt

Asymmetry of the Less-Than Relation on Integers

Informal description

For any integers $a$ and $b$, if $a < b$ then it is not the case that $b < a$.

Int.le_of_eq theorem

(hab : a = b) : a ≤ b

Full source

protected lemma le_of_eq (hab : a = b) : a ≤ b := by rw [hab]; exact Int.le_rfl

Equality Implies Less-Than-or-Equal for Integers

Informal description

For any integers $a$ and $b$, if $a = b$ then $a \leq b$.

Int.ge_of_eq theorem

(hab : a = b) : b ≤ a

Full source

protected lemma ge_of_eq (hab : a = b) : b ≤ a := Int.le_of_eq hab.symm

Equality Implies Greater-Than-or-Equal for Integers

Informal description

For any integers $a$ and $b$, if $a = b$ then $b \leq a$.

Int.le_antisymm_iff theorem

: a = b ↔ a ≤ b ∧ b ≤ a

Full source

protected lemma le_antisymm_iff : a = b ↔ a ≤ b ∧ b ≤ a :=
  ⟨fun h ↦ ⟨Int.le_of_eq h, Int.ge_of_eq h⟩, fun h ↦ Int.le_antisymm h.1 h.2⟩

Antisymmetry of Integer Ordering: $a = b \leftrightarrow (a \leq b \land b \leq a)$

Informal description

For any integers $a$ and $b$, the equality $a = b$ holds if and only if both $a \leq b$ and $b \leq a$ are true.

Int.le_iff_eq_or_lt theorem

: a ≤ b ↔ a = b ∨ a < b

Full source

protected lemma le_iff_eq_or_lt : a ≤ b ↔ a = b ∨ a < b := by omega

Characterization of Integer Ordering: $a \leq b$ as Equality or Strict Inequality

Informal description

For any integers $a$ and $b$, the inequality $a \leq b$ holds if and only if either $a = b$ or $a < b$.

Int.le_iff_lt_or_eq theorem

: a ≤ b ↔ a < b ∨ a = b

Full source

protected lemma le_iff_lt_or_eq : a ≤ b ↔ a < b ∨ a = b := by rw [Int.le_iff_eq_or_lt, or_comm]

Characterization of Integer Ordering: $a \leq b$ as Strict Inequality or Equality

Informal description

For any integers $a$ and $b$, the inequality $a \leq b$ holds if and only if either $a < b$ or $a = b$.

Int.one_pos theorem

: 0 < (1 : Int)

Full source

protected lemma one_pos : 0 < (1 : Int) := Int.zero_lt_one

Positivity of One in Integers: $0 < 1$

Informal description

The integer $1$ is strictly greater than $0$, i.e., $0 < 1$.

Int.one_ne_zero theorem

: (1 : ℤ) ≠ 0

Full source

protected lemma one_ne_zero : (1 : ℤ) ≠ 0 := by decide

Non-Equality of One and Zero in Integers

Informal description

The integer $1$ is not equal to $0$, i.e., $1 \neq 0$.

Int.one_nonneg theorem

: 0 ≤ (1 : ℤ)

Full source

protected lemma one_nonneg : 0 ≤ (1 : ℤ) := Int.le_of_lt Int.zero_lt_one

Nonnegativity of One in Integers

Informal description

The integer $1$ is nonnegative, i.e., $0 \leq 1$.

Int.neg_eq_neg theorem

{a b : ℤ} (h : -a = -b) : a = b

Full source

protected theorem neg_eq_neg {a b : ℤ} (h : -a = -b) : a = b := Int.neg_inj.1 h

Negation Preserves Equality in Integers

Informal description

For any integers $a$ and $b$, if $-a = -b$, then $a = b$.

Int.neg_pos theorem

: 0 < -a ↔ a < 0

Full source

@[simp high]
protected lemma neg_pos : 0 < -a ↔ a < 0 := ⟨Int.neg_of_neg_pos, Int.neg_pos_of_neg⟩

Negation Positivity Equivalence for Integers

Informal description

For any integer $a$, the negation $-a$ is positive if and only if $a$ is negative, i.e., $0 < -a \leftrightarrow a < 0$.

Int.neg_nonneg theorem

: 0 ≤ -a ↔ a ≤ 0

Full source

@[simp high]
protected lemma neg_nonneg : 0 ≤ -a ↔ a ≤ 0 := ⟨Int.nonpos_of_neg_nonneg, Int.neg_nonneg_of_nonpos⟩

Negation Preserves Nonnegativity and Nonpositivity in Integers

Informal description

For any integer $a$, the negation $-a$ is nonnegative if and only if $a$ is nonpositive, i.e., $0 \leq -a \leftrightarrow a \leq 0$.

Int.neg_neg_iff_pos theorem

: -a < 0 ↔ 0 < a

Full source

@[simp high]
protected lemma neg_neg_iff_pos : -a < 0 ↔ 0 < a := ⟨Int.pos_of_neg_neg, Int.neg_neg_of_pos⟩

Negation Sign Reversal: $-a < 0 \leftrightarrow 0 < a$

Informal description

For any integer $a$, the negation $-a$ is less than zero if and only if $a$ is greater than zero, i.e., $-a < 0 \leftrightarrow 0 < a$.

Int.sub_pos theorem

: 0 < a - b ↔ b < a

Full source

@[simp high]
protected lemma sub_pos : 0 < a - b ↔ b < a := ⟨Int.lt_of_sub_pos, Int.sub_pos_of_lt⟩

Positivity of Integer Difference Characterizes Ordering

Informal description

For any integers $a$ and $b$, the difference $a - b$ is positive if and only if $b$ is less than $a$, i.e., $0 < a - b \leftrightarrow b < a$.

Int.sub_nonneg theorem

: 0 ≤ a - b ↔ b ≤ a

Full source

@[simp high]
protected lemma sub_nonneg : 0 ≤ a - b ↔ b ≤ a := ⟨Int.le_of_sub_nonneg, Int.sub_nonneg_of_le⟩

Nonnegativity of Integer Difference Characterizes Order Relation

Informal description

For any integers $a$ and $b$, the difference $a - b$ is nonnegative if and only if $b$ is less than or equal to $a$, i.e., $0 \leq a - b \leftrightarrow b \leq a$.

Int.ofNat_add_out theorem

(m n : ℕ) : ↑m + ↑n = (↑(m + n) : ℤ)

Full source

protected theorem ofNat_add_out (m n : ℕ) : ↑m + ↑n = (↑(m + n) : ℤ) := rfl

Integer Embedding Preserves Addition of Natural Numbers

Informal description

For any natural numbers $m$ and $n$, the sum of their canonical integer embeddings equals the integer embedding of their sum, i.e., $m_\mathbb{Z} + n_\mathbb{Z} = (m + n)_\mathbb{Z}$.

Int.ofNat_mul_out theorem

(m n : ℕ) : ↑m * ↑n = (↑(m * n) : ℤ)

Full source

protected theorem ofNat_mul_out (m n : ℕ) : ↑m * ↑n = (↑(m * n) : ℤ) := rfl

Integer Embedding Preserves Multiplication of Natural Numbers

Informal description

For any natural numbers $m$ and $n$, the product of their canonical integer embeddings equals the canonical integer embedding of their product, i.e., $m \cdot n = (m \cdot n)_{\mathbb{Z}}$.

Int.ofNat_add_one_out theorem

(n : ℕ) : ↑n + (1 : ℤ) = ↑(succ n)

Full source

protected theorem ofNat_add_one_out (n : ℕ) : ↑n + (1 : ℤ) = ↑(succ n) := rfl

Integer Cast of Successor Equals Integer Cast Plus One

Informal description

For any natural number $n$, the integer obtained by casting $n$ to $\mathbb{Z}$ and adding 1 is equal to the integer obtained by casting the successor of $n$ to $\mathbb{Z}$. In other words, $n + 1 = (n + 1)$ as integers.

Int.ofNat_eq_natCast theorem

(n : ℕ) : Int.ofNat n = n

Full source

@[simp] lemma ofNat_eq_natCast (n : ℕ) : Int.ofNat n = n := rfl

Equality of Natural Number Embedding and Integer Cast

Informal description

For any natural number $n$, the canonical embedding of $n$ into the integers (via `Int.ofNat`) is equal to the integer cast of $n$ (denoted by the coercion `↑n`).

Int.natCast_inj theorem

{m n : ℕ} : (m : ℤ) = (n : ℤ) ↔ m = n

Full source

@[norm_cast] lemma natCast_inj {m n : ℕ} : (m : ℤ) = (n : ℤ) ↔ m = n := ofNat_inj

Injectivity of Natural Number to Integer Casting

Informal description

For any natural numbers $m$ and $n$, the integer cast of $m$ equals the integer cast of $n$ if and only if $m = n$.

Int.natAbs_cast theorem

(n : ℕ) : natAbs ↑n = n

Full source

@[simp, norm_cast] lemma natAbs_cast (n : ℕ) : natAbs ↑n = n := rfl

Absolute Value of Natural Number Cast to Integer Equals Itself

Informal description

For any natural number $n$, the absolute value of the integer cast of $n$ is equal to $n$ itself, i.e., $\text{natAbs}(n) = n$.

Int.natCast_sub theorem

{n m : ℕ} : n ≤ m → (↑(m - n) : ℤ) = ↑m - ↑n

Full source

@[norm_cast]
protected lemma natCast_sub {n m : ℕ} : n ≤ m → (↑(m - n) : ℤ) = ↑m - ↑n := ofNat_sub

Integer Subtraction Preserves Natural Number Subtraction Under Casting

Informal description

For any natural numbers $n$ and $m$ such that $n \leq m$, the integer obtained by casting the natural number subtraction $m - n$ is equal to the integer subtraction of the casts of $m$ and $n$, i.e., $(m - n : \mathbb{Z}) = (m : \mathbb{Z}) - (n : \mathbb{Z})$.

Int.natCast_eq_zero theorem

{n : ℕ} : (n : ℤ) = 0 ↔ n = 0

Full source

@[simp high] lemma natCast_eq_zero {n : ℕ} : (n : ℤ) = 0 ↔ n = 0 := by omega

Integer Cast of Natural Number Equals Zero if and Only if Natural Number is Zero

Informal description

For any natural number $n$, the integer cast of $n$ equals zero if and only if $n$ equals zero, i.e., $(n : \mathbb{Z}) = 0 \leftrightarrow n = 0$.

Int.natCast_ne_zero theorem

{n : ℕ} : (n : ℤ) ≠ 0 ↔ n ≠ 0

Full source

lemma natCast_ne_zero {n : ℕ} : (n : ℤ) ≠ 0(n : ℤ) ≠ 0 ↔ n ≠ 0 := by omega

Nonzero Integer Cast of Natural Number is Nonzero

Informal description

For any natural number $n$, the integer cast of $n$ is nonzero if and only if $n$ is nonzero.

Int.natCast_ne_zero_iff_pos theorem

{n : ℕ} : (n : ℤ) ≠ 0 ↔ 0 < n

Full source

lemma natCast_ne_zero_iff_pos {n : ℕ} : (n : ℤ) ≠ 0(n : ℤ) ≠ 0 ↔ 0 < n := by omega

Nonzero Integer Cast of Natural Number is Positive

Informal description

For any natural number $n$, the integer cast of $n$ is nonzero if and only if $n$ is positive, i.e., $(n : \mathbb{Z}) \neq 0 \leftrightarrow 0 < n$.

Int.natCast_pos theorem

{n : ℕ} : (0 : ℤ) < n ↔ 0 < n

Full source

@[simp high] lemma natCast_pos {n : ℕ} : (0 : ℤ) < n ↔ 0 < n := by omega

Positivity of Natural Number Cast to Integers: $0 < (n : \mathbb{Z}) \leftrightarrow 0 < n$

Informal description

For any natural number $n$, the integer $0$ is less than the cast of $n$ to $\mathbb{Z}$ if and only if $0 < n$ in $\mathbb{N}$.

Int.natCast_succ_pos theorem

(n : ℕ) : 0 < (n.succ : ℤ)

Full source

lemma natCast_succ_pos (n : ℕ) : 0 < (n.succ : ℤ) := natCast_pos.2 n.succ_pos

Positivity of Successor Cast to Integers: $0 < (n+1 : \mathbb{Z})$

Informal description

For any natural number $n$, the integer cast of the successor of $n$ is positive, i.e., $0 < (n+1 : \mathbb{Z})$.

Int.natCast_nonpos_iff theorem

{n : ℕ} : (n : ℤ) ≤ 0 ↔ n = 0

Full source

@[simp high] lemma natCast_nonpos_iff {n : ℕ} : (n : ℤ) ≤ 0 ↔ n = 0 := by omega

Integer Cast of Natural Number is Nonpositive iff Zero

Informal description

For any natural number $n$, the integer cast of $n$ is less than or equal to zero if and only if $n$ is equal to zero, i.e., $(n : \mathbb{Z}) \leq 0 \leftrightarrow n = 0$.

Int.natCast_nonneg theorem

(n : ℕ) : 0 ≤ (n : ℤ)

Full source

lemma natCast_nonneg (n : ℕ) : 0 ≤ (n : ℤ) := ofNat_le.2 (Nat.zero_le _)

Nonnegativity of Natural Number Cast to Integers

Informal description

For any natural number $n$, the integer cast of $n$ is nonnegative, i.e., $0 \leq (n : \mathbb{Z})$.

Int.sign_natCast_add_one theorem

(n : ℕ) : sign (n + 1) = 1

Full source

@[simp] lemma sign_natCast_add_one (n : ℕ) : sign (n + 1) = 1 := rfl

Sign of Successor of Natural Number Cast to Integer is One

Informal description

For any natural number $n$, the sign of the integer $n + 1$ is equal to $1$.

Int.cast_id theorem

{n : ℤ} : Int.cast n = n

Full source

@[simp, norm_cast] lemma cast_id {n : ℤ} : Int.cast n = n := rfl

Identity of Integer Casting

Informal description

For any integer $n$, the canonical embedding of $n$ into the integers (via `Int.cast`) is equal to $n$ itself, i.e., $\text{cast}(n) = n$.

Int.two_mul theorem

: ∀ n : ℤ, 2 * n = n + n

Full source

protected lemma two_mul : ∀ n : ℤ, 2 * n = n + n
  | (n : ℕ) => by norm_cast; exact n.two_mul
  | -[n+1] => by
    change (2 : ℕ) * (_ : ℤ) = _
    rw [Int.ofNat_mul_negSucc, Nat.two_mul, ofNat_add, Int.neg_add]
    rfl

Double of an Integer Equals Its Sum with Itself

Informal description

For any integer $n$, twice $n$ is equal to the sum of $n$ with itself, i.e., $2n = n + n$.

Int.mul_le_mul_iff_of_pos_right theorem

(ha : 0 < a) : b * a ≤ c * a ↔ b ≤ c

Full source

protected lemma mul_le_mul_iff_of_pos_right (ha : 0 < a) : b * a ≤ c * a ↔ b ≤ c :=
  ⟨(le_of_mul_le_mul_right · ha), (Int.mul_le_mul_of_nonneg_right · (Int.le_of_lt ha))⟩

Multiplication Preserves Order for Positive Integers

Informal description

For any integer $a > 0$, the inequality $b \cdot a \leq c \cdot a$ holds if and only if $b \leq c$.

Int.mul_nonneg_iff_of_pos_right theorem

(hb : 0 < b) : 0 ≤ a * b ↔ 0 ≤ a

Full source

protected lemma mul_nonneg_iff_of_pos_right (hb : 0 < b) : 0 ≤ a * b ↔ 0 ≤ a := by
  simpa using (Int.mul_le_mul_iff_of_pos_right hb : 0 * b ≤ a * b ↔ 0 ≤ a)

Nonnegativity of Product with Positive Integer

Informal description

For any integer $b > 0$, the product $a \cdot b$ is nonnegative if and only if $a$ is nonnegative, i.e., $0 \leq a \cdot b \leftrightarrow 0 \leq a$.

Int.succ definition

(a : ℤ)

Full source

/-- Immediate successor of an integer: `succ n = n + 1` -/
def succ (a : ℤ) := a + 1

Successor function on integers

Informal description

The successor function on integers, defined by $\text{succ}(a) = a + 1$ for any integer $a$.

Int.pred definition

(a : ℤ)

Full source

/-- Immediate predecessor of an integer: `pred n = n - 1` -/
def pred (a : ℤ) := a - 1

Integer predecessor function

Informal description

The predecessor function on integers, defined by $\operatorname{pred}(a) = a - 1$ for any integer $a$.

Int.pred_succ theorem

(a : ℤ) : pred (succ a) = a

Full source

lemma pred_succ (a : ℤ) : pred (succ a) = a := Int.add_sub_cancel _ _

Predecessor of Successor is Identity for Integers

Informal description

For any integer $a$, the predecessor of the successor of $a$ equals $a$, i.e., $\operatorname{pred}(\operatorname{succ}(a)) = a$.

Int.succ_pred theorem

(a : ℤ) : succ (pred a) = a

Full source

lemma succ_pred (a : ℤ) : succ (pred a) = a := Int.sub_add_cancel _ _

Successor of Predecessor Equals Original Integer

Informal description

For any integer $a$, the successor of the predecessor of $a$ equals $a$, i.e., $\operatorname{succ}(\operatorname{pred}(a)) = a$.

Int.neg_succ theorem

(a : ℤ) : -succ a = pred (-a)

Full source

lemma neg_succ (a : ℤ) : -succ a = pred (-a) := Int.neg_add

Negation of Successor Equals Predecessor of Negation

Informal description

For any integer $a$, the negation of its successor equals the predecessor of its negation, i.e., $-(\text{succ}(a)) = \text{pred}(-a)$.

Int.succ_neg_succ theorem

(a : ℤ) : succ (-succ a) = -a

Full source

lemma succ_neg_succ (a : ℤ) : succ (-succ a) = -a := by rw [neg_succ, succ_pred]

Successor of Negated Successor Equals Negation

Informal description

For any integer $a$, the successor of the negation of the successor of $a$ equals the negation of $a$, i.e., $\operatorname{succ}(-(\operatorname{succ}(a))) = -a$.

Int.neg_pred theorem

(a : ℤ) : -pred a = succ (-a)

Full source

lemma neg_pred (a : ℤ) : -pred a = succ (-a) := by
  rw [← Int.neg_eq_comm.mp (neg_succ (-a)), Int.neg_neg]

Negation of Predecessor Equals Successor of Negation

Informal description

For any integer $a$, the negation of its predecessor equals the successor of its negation, i.e., $-(\text{pred}(a)) = \text{succ}(-a)$.

Int.pred_neg_pred theorem

(a : ℤ) : pred (-pred a) = -a

Full source

lemma pred_neg_pred (a : ℤ) : pred (-pred a) = -a := by rw [neg_pred, pred_succ]

Predecessor of Negated Predecessor Equals Negation

Informal description

For any integer $a$, the predecessor of the negation of its predecessor equals the negation of $a$, i.e., $\operatorname{pred}(-(\operatorname{pred}(a))) = -a$.

Int.pred_nat_succ theorem

(n : ℕ) : pred (Nat.succ n) = n

Full source

lemma pred_nat_succ (n : ℕ) : pred (Nat.succ n) = n := pred_succ n

Predecessor of Successor is Identity for Natural Numbers as Integers

Informal description

For any natural number $n$, the predecessor of the integer successor of $n$ equals $n$, i.e., $\operatorname{pred}(\operatorname{succ}(n)) = n$.

Int.neg_nat_succ theorem

(n : ℕ) : -(Nat.succ n : ℤ) = pred (-n)

Full source

lemma neg_nat_succ (n : ℕ) : -(Nat.succ n : ℤ) = pred (-n) := neg_succ n

Negation of Successor Equals Predecessor of Negation for Natural Numbers

Informal description

For any natural number $n$, the negation of the integer successor of $n$ equals the predecessor of the negation of $n$, i.e., $-(\text{succ}(n)) = \text{pred}(-n)$.

Int.succ_neg_natCast_succ theorem

(n : ℕ) : succ (-Nat.succ n) = -n

Full source

lemma succ_neg_natCast_succ (n : ℕ) : succ (-Nat.succ n) = -n := succ_neg_succ n

Successor of Negated Successor of Natural Number Equals Negation

Informal description

For any natural number $n$, the successor of the negation of the successor of $n$ equals the negation of $n$, i.e., $\operatorname{succ}(-(\operatorname{succ}(n))) = -n$.

Int.natCast_pred_of_pos theorem

{n : ℕ} (h : 0 < n) : ((n - 1 : ℕ) : ℤ) = (n : ℤ) - 1

Full source

@[norm_cast] lemma natCast_pred_of_pos {n : ℕ} (h : 0 < n) : ((n - 1 : ℕ) : ℤ) = (n : ℤ) - 1 := by
  cases n; cases h; simp [ofNat_succ]

Integer Cast of Predecessor Equals Integer Cast Minus One

Informal description

For any positive natural number $n$, the integer obtained by casting the predecessor of $n$ (i.e., $n - 1$) is equal to the integer obtained by casting $n$ and then subtracting $1$. In symbols: $(n - 1 : ℤ) = (n : ℤ) - 1$.

Int.lt_succ_self theorem

(a : ℤ) : a < succ a

Full source

lemma lt_succ_self (a : ℤ) : a < succ a := by unfold succ; omega

Integer Successor Inequality: $a < a + 1$

Informal description

For any integer $a$, we have $a < a + 1$.

Int.pred_self_lt theorem

(a : ℤ) : pred a < a

Full source

lemma pred_self_lt (a : ℤ) : pred a < a := by unfold pred; omega

Predecessor is Strictly Less Than Original Integer

Informal description

For any integer $a$, the predecessor of $a$ is strictly less than $a$, i.e., $\operatorname{pred}(a) < a$.

Int.le_add_one_iff theorem

: m ≤ n + 1 ↔ m ≤ n ∨ m = n + 1

Full source

lemma le_add_one_iff : m ≤ n + 1 ↔ m ≤ n ∨ m = n + 1 := by omega

Integer Inequality: $m \leq n + 1 \leftrightarrow m \leq n \lor m = n + 1$

Informal description

For any integers $m$ and $n$, the inequality $m \leq n + 1$ holds if and only if either $m \leq n$ or $m = n + 1$.

Int.sub_one_lt_iff theorem

: m - 1 < n ↔ m ≤ n

Full source

lemma sub_one_lt_iff : m - 1 < n ↔ m ≤ n := by omega

Subtraction-One Inequality Equivalence for Integers

Informal description

For any integers $m$ and $n$, the inequality $m - 1 < n$ holds if and only if $m \leq n$.

Int.le_sub_one_iff theorem

: m ≤ n - 1 ↔ m < n

Full source

lemma le_sub_one_iff : m ≤ n - 1 ↔ m < n := by omega

Integer Inequality: $m \leq n - 1 \leftrightarrow m < n$

Informal description

For any integers $m$ and $n$, the inequality $m \leq n - 1$ holds if and only if $m < n$.

Int.add_le_iff_le_sub theorem

: a + b ≤ c ↔ a ≤ c - b

Full source

protected lemma add_le_iff_le_sub : a + b ≤ c ↔ a ≤ c - b := add_le_iff_le_sub ..

Addition-Subtraction Inequality Equivalence for Integers

Informal description

For any integers $a$, $b$, and $c$, the inequality $a + b \leq c$ holds if and only if $a \leq c - b$.

Int.le_add_iff_sub_le theorem

: a ≤ b + c ↔ a - c ≤ b

Full source

protected lemma le_add_iff_sub_le : a ≤ b + c ↔ a - c ≤ b := le_add_iff_sub_le ..

Inequality Transformation via Subtraction: $a \leq b + c \leftrightarrow a - c \leq b$

Informal description

For any integers $a$, $b$, and $c$, the inequality $a \leq b + c$ holds if and only if $a - c \leq b$.

Int.add_le_zero_iff_le_neg theorem

: a + b ≤ 0 ↔ a ≤ -b

Full source

protected lemma add_le_zero_iff_le_neg : a + b ≤ 0 ↔ a ≤ - b := add_le_zero_iff_le_neg ..

Sum Nonpositive iff First Term Bounded by Negative of Second Term

Informal description

For any integers $a$ and $b$, the sum $a + b$ is less than or equal to zero if and only if $a$ is less than or equal to $-b$.

Int.add_le_zero_iff_le_neg' theorem

: a + b ≤ 0 ↔ b ≤ -a

Full source

protected lemma add_le_zero_iff_le_neg' : a + b ≤ 0 ↔ b ≤ -a := add_le_zero_iff_le_neg' ..

Sum Nonpositive iff Second Term Bounded by Negative of First Term

Informal description

For any integers $a$ and $b$, the sum $a + b$ is less than or equal to zero if and only if $b$ is less than or equal to $-a$.

Int.add_nonnneg_iff_neg_le theorem

: 0 ≤ a + b ↔ -b ≤ a

Full source

protected lemma add_nonnneg_iff_neg_le : 0 ≤ a + b ↔ -b ≤ a := add_nonnneg_iff_neg_le ..

Sum Nonnegative iff Negative of Second Term Bounded by First Term

Informal description

For any integers $a$ and $b$, the sum $a + b$ is nonnegative if and only if $-b$ is less than or equal to $a$.

Int.add_nonnneg_iff_neg_le' theorem

: 0 ≤ a + b ↔ -a ≤ b

Full source

protected lemma add_nonnneg_iff_neg_le' : 0 ≤ a + b ↔ -a ≤ b := add_nonnneg_iff_neg_le' ..

Sum Nonnegative iff Negative of First Term Bounded by Second Term

Informal description

For any integers $a$ and $b$, the sum $a + b$ is nonnegative if and only if $-a$ is less than or equal to $b$.

Int.induction_on theorem

 {p : ℤ → Prop} (i : ℤ) (hz : p 0) (hp : ∀ i : ℕ, p i → p (i + 1)) (hn : ∀ i : ℕ, p (-i) → p (-i - 1)) : p i

Full source

/--
Induction on integers: prove a proposition `p i` by proving the base case `p 0`,
the upwards induction step `p i → p (i + 1)` and the downwards induction step `p (-i) → p (-i - 1)`.

It is used as the default induction principle for the `induction` tactic.
-/
@[elab_as_elim, induction_eliminator] protected lemma induction_on {p : ℤ → Prop} (i : ℤ)
    (hz : p 0) (hp : ∀ i : ℕ, p i → p (i + 1)) (hn : ∀ i : ℕ, p (-i) → p (-i - 1)) : p i := by
  cases i with
  | ofNat i =>
    induction i with
    | zero => exact hz
    | succ i ih => exact hp _ ih
  | negSucc i =>
    suffices ∀ n : ℕ, p (-n) from this (i + 1)
    intro n; induction n with
    | zero => simp [hz]
    | succ n ih => simpa [Int.natCast_succ, Int.neg_add, Int.sub_eq_add_neg] using hn _ ih

Integer Induction Principle (Bidirectional)

Informal description

Let $p$ be a predicate on integers. To prove $p(i)$ holds for all integers $i$, it suffices to: 1. Prove the base case $p(0)$, 2. Prove the upward induction step: for any natural number $i$, $p(i)$ implies $p(i + 1)$, 3. Prove the downward induction step: for any natural number $i$, $p(-i)$ implies $p(-i - 1)$.

Int.inductionOn' definition

: C z

Full source

/-- Inductively define a function on `ℤ` by defining it at `b`, for the `succ` of a number greater
than `b`, and the `pred` of a number less than `b`. -/
@[elab_as_elim] protected def inductionOn' : C z :=
  cast (congrArg C <| show b + (z - b) = z by rw [Int.add_comm, z.sub_add_cancel b]) <|
  match z - b with
  | .ofNat n => pos n
  | .negSucc n => neg n
where
  /-- The positive case of `Int.inductionOn'`. -/
  pos : ∀ n : ℕ, C (b + n)
  | 0 => cast (by simp) H0
  | n+1 => cast (by rw [Int.add_assoc]; rfl) <|
    Hs _ (Int.le_add_of_nonneg_right (ofNat_nonneg _)) (pos n)

  /-- The negative case of `Int.inductionOn'`. -/
  neg : ∀ n : ℕ, C (b + -[n+1])
  | 0 => Hp _ Int.le_rfl H0
  | n+1 => by
    refine cast (by rw [Int.add_sub_assoc]; rfl) (Hp _ (Int.le_of_lt ?_) (neg n))
    omega

Integer induction from a base point

Informal description

Given an integer $b$ and a predicate $C$ on integers, the function `Int.inductionOn'` defines $C(z)$ for any integer $z$ by induction, starting from $b$. It handles three cases: 1. Base case: $C(b)$ is defined directly. 2. Successor case: For $z > b$, $C(z)$ is defined in terms of $C(z-1)$. 3. Predecessor case: For $z < b$, $C(z)$ is defined in terms of $C(z+1)$. More precisely, for any integer $z$, the value $C(z)$ is computed by: - If $z = b + n$ for some natural number $n$, then $C(z)$ is defined by induction on $n$ using the successor function $Hs$. - If $z = b - (n+1)$ for some natural number $n$, then $C(z)$ is defined by induction on $n$ using the predecessor function $Hp$.

Int.inductionOn'_self theorem

: b.inductionOn' b H0 Hs Hp = H0

Full source

lemma inductionOn'_self : b.inductionOn' b H0 Hs Hp = H0 :=
  cast_eq_iff_heq.mpr <| .symm <| by rw [b.sub_self, ← cast_eq_iff_heq]; rfl

Base Case of Integer Induction from Base Point

Informal description

For any integer $b$ and functions $H0$, $Hs$, $Hp$ defining the induction steps, the induction from base point $b$ evaluated at $b$ itself equals $H0$.

Int.inductionOn'_sub_one theorem

(hz : z ≤ b) : (z - 1).inductionOn' b H0 Hs Hp = Hp z hz (z.inductionOn' b H0 Hs Hp)

Full source

lemma inductionOn'_sub_one (hz : z ≤ b) :
    (z - 1).inductionOn' b H0 Hs Hp = Hp z hz (z.inductionOn' b H0 Hs Hp) := by
  apply cast_eq_iff_heq.mpr
  obtain ⟨n, hn⟩ := Int.eq_negSucc_of_lt_zero (show z - 1 - b < 0 by omega)
  rw [hn]
  obtain _|n := n
  · change _ = -1 at hn
    have : z = b := by omega
    subst this; rw [inductionOn'_self]; exact heq_of_eq rfl
  · have : z = b + -[n+1] := by rw [Int.negSucc_eq] at hn ⊢; omega
    subst this
    refine (cast_heq _ _).trans ?_
    congr
    symm
    rw [Int.inductionOn', cast_eq_iff_heq, show b + -[n+1] - b = -[n+1] by omega]

Predecessor Case of Integer Induction from Base Point

Informal description

For any integer $z$ and base integer $b$ such that $z \leq b$, the induction from base point $b$ evaluated at $z - 1$ equals the predecessor function $Hp$ applied to $z$, the proof $hz$ that $z \leq b$, and the induction from base point $b$ evaluated at $z$. That is, $(z - 1).\text{inductionOn}'\, b\, H0\, Hs\, Hp = Hp\, z\, hz\, (z.\text{inductionOn}'\, b\, H0\, Hs\, Hp)$.

Int.negInduction definition

{C : ℤ → Sort*} (nat : ∀ n : ℕ, C n) (neg : (∀ n : ℕ, C n) → ∀ n : ℕ, C (-n)) : ∀ n : ℤ, C n

Full source

/-- Inductively define a function on `ℤ` by defining it on `ℕ` and extending it from `n` to `-n`. -/
@[elab_as_elim] protected def negInduction {C : ℤ → Sort*} (nat : ∀ n : ℕ, C n)
    (neg : (∀ n : ℕ, C n) → ∀ n : ℕ, C (-n)) : ∀ n : ℤ, C n
  | .ofNat n => nat n
  | .negSucc n => neg nat <| n + 1

Inductive definition on integers via extension from naturals to negatives

Informal description

Given a type family $C$ on the integers, a function `nat` that defines $C$ on natural numbers, and a function `neg` that extends the definition of $C$ from positive integers to negative integers using `nat`, the function `Int.negInduction` defines $C$ for all integers $n$. Specifically: - For non-negative integers (of the form `n : ℕ`), it applies `nat n`. - For negative integers (of the form `-n-1`), it applies `neg nat (n+1)`.

Int.le_induction theorem

{P : ℤ → Prop} {m : ℤ} (h0 : P m) (h1 : ∀ n : ℤ, m ≤ n → P n → P (n + 1)) (n : ℤ) : m ≤ n → P n

Full source

/-- See `Int.inductionOn'` for an induction in both directions. -/
protected lemma le_induction {P : ℤ → Prop} {m : ℤ} (h0 : P m)
    (h1 : ∀ n : ℤ, m ≤ n → P n → P (n + 1)) (n : ℤ) : m ≤ n → P n := by
  refine Int.inductionOn' n m ?_ ?_ ?_
  · intro
    exact h0
  · intro k hle hi _
    exact h1 k hle (hi hle)
  · intro k hle _ hle'
    omega

Upward Integer Induction Principle

Informal description

Let $P$ be a predicate on integers and let $m$ be an integer. If $P(m)$ holds and for every integer $n \geq m$, $P(n)$ implies $P(n + 1)$, then $P(n)$ holds for all integers $n \geq m$.

Int.le_induction_down theorem

{P : ℤ → Prop} {m : ℤ} (h0 : P m) (h1 : ∀ n : ℤ, n ≤ m → P n → P (n - 1)) (n : ℤ) : n ≤ m → P n

Full source

/-- See `Int.inductionOn'` for an induction in both directions. -/
protected theorem le_induction_down {P : ℤ → Prop} {m : ℤ} (h0 : P m)
    (h1 : ∀ n : ℤ, n ≤ m → P n → P (n - 1)) (n : ℤ) : n ≤ m → P n :=
  Int.inductionOn' n m (fun _ ↦ h0) (fun k hle _ hle' ↦ by omega)
    fun k hle hi _ ↦ h1 k hle (hi hle)

Downward Integer Induction Principle

Informal description

Let $P$ be a predicate on integers and let $m$ be an integer. If $P(m)$ holds and for every integer $n \leq m$, $P(n)$ implies $P(n - 1)$, then $P(n)$ holds for all integers $n \leq m$.

Int.strongRec definition

(n : ℤ) : P n

Full source

/-- A strong recursor for `Int` that specifies explicit values for integers below a threshold,
and is analogous to `Nat.strongRec` for integers on or above the threshold. -/
@[elab_as_elim] protected def strongRec (n : ℤ) : P n := by
  refine if hnm : n < m then lt n hnm else ge n (by omega) (n.inductionOn' m lt ?_ ?_)
  · intro _n _ ih l _
    exact if hlm : l < m then lt l hlm else ge l (by omega) fun k _ ↦ ih k (by omega)
  · exact fun n _ hn l _ ↦ hn l (by omega)

Strong Recursion Principle for Integers

Informal description

The strong recursion principle for integers, which defines a predicate $P(n)$ for all integers $n$ by specifying: 1. For integers $n < m$, $P(n)$ is given explicitly. 2. For integers $n \geq m$, $P(n)$ is defined by induction on $n$ using a successor function. 3. For integers $n \leq m$, $P(n)$ is defined by induction on $n$ using a predecessor function.

Int.strongRec_of_lt theorem

(hn : n < m) : m.strongRec lt ge n = lt n hn

Full source

lemma strongRec_of_lt (hn : n < m) : m.strongRec lt ge n = lt n hn := dif_pos _

Strong Recursion Evaluation for Integers Below Base Case

Informal description

For any integers $n$ and $m$ with $n < m$, the strong recursion function `m.strongRec` evaluated at $n$ equals the left case function `lt` applied to $n$ and the proof `hn` that $n < m$.

Int.mul_le_mul_left theorem

(ha : 0 < a) : a * b ≤ a * c ↔ b ≤ c

Full source

@[simp high] protected lemma mul_le_mul_left (ha : 0 < a) : a * b ≤ a * c ↔ b ≤ c where
  mp hbc := Int.le_of_mul_le_mul_left hbc ha
  mpr hbc := Int.mul_le_mul_of_nonneg_left hbc <| Int.le_of_lt ha

Left Multiplication Preserves Order for Positive Integers

Informal description

For any integer $a > 0$ and integers $b, c$, the inequality $a \cdot b \leq a \cdot c$ holds if and only if $b \leq c$.

Int.mul_le_mul_right theorem

(ha : 0 < a) : b * a ≤ c * a ↔ b ≤ c

Full source

@[simp high] protected lemma mul_le_mul_right (ha : 0 < a) : b * a ≤ c * a ↔ b ≤ c where
  mp hbc := Int.le_of_mul_le_mul_right hbc ha
  mpr hbc := Int.mul_le_mul_of_nonneg_right hbc <| Int.le_of_lt ha

Right Multiplication Preserves Order for Positive Integers

Informal description

For any integers $a$, $b$, and $c$, if $a > 0$, then the inequality $b \cdot a \leq c \cdot a$ holds if and only if $b \leq c$.

Int.mul_lt_mul_left theorem

(ha : 0 < a) : a * b < a * c ↔ b < c

Full source

@[simp high] protected lemma mul_lt_mul_left (ha : 0 < a) : a * b < a * c ↔ b < c where
  mp hbc := Int.lt_of_mul_lt_mul_left hbc <| Int.le_of_lt ha
  mpr hbc := Int.mul_lt_mul_of_pos_left hbc ha

Left Multiplication Preserves Strict Inequality for Positive Integers

Informal description

For any integer $a > 0$ and integers $b, c$, the inequality $a \cdot b < a \cdot c$ holds if and only if $b < c$.

Int.mul_lt_mul_right theorem

(ha : 0 < a) : b * a < c * a ↔ b < c

Full source

@[simp high] protected lemma mul_lt_mul_right (ha : 0 < a) : b * a < c * a ↔ b < c where
  mp hbc := Int.lt_of_mul_lt_mul_right hbc <| Int.le_of_lt ha
  mpr hbc := Int.mul_lt_mul_of_pos_right hbc ha

Right Multiplication Preserves Strict Inequality for Positive Integers

Informal description

For any integers $a$, $b$, and $c$ with $a > 0$, the inequality $b \cdot a < c \cdot a$ holds if and only if $b < c$.

Int.mul_le_mul_left_of_neg theorem

(ha : a < 0) : a * b ≤ a * c ↔ c ≤ b

Full source

@[simp high] protected lemma mul_le_mul_left_of_neg (ha : a < 0) :
    a * b ≤ a * c ↔ c ≤ b := by
  rw [← Int.neg_le_neg_iff, Int.neg_mul_eq_neg_mul, Int.neg_mul_eq_neg_mul,
    Int.mul_le_mul_left <| Int.neg_pos.2 ha]

Left Multiplication Reverses Order for Negative Integers: $a \cdot b \leq a \cdot c \leftrightarrow c \leq b$

Informal description

For any integer $a < 0$ and integers $b, c$, the inequality $a \cdot b \leq a \cdot c$ holds if and only if $c \leq b$.

Int.mul_le_mul_right_of_neg theorem

(ha : a < 0) : b * a ≤ c * a ↔ c ≤ b

Full source

@[simp high] protected lemma mul_le_mul_right_of_neg (ha : a < 0) :
    b * a ≤ c * a ↔ c ≤ b := by
  rw [← Int.neg_le_neg_iff, Int.neg_mul_eq_mul_neg, Int.neg_mul_eq_mul_neg,
    Int.mul_le_mul_right <| Int.neg_pos.2 ha]

Right Multiplication Reverses Order for Negative Integers

Informal description

For any integers $a$, $b$, and $c$ with $a < 0$, the inequality $b \cdot a \leq c \cdot a$ holds if and only if $c \leq b$.

Int.mul_lt_mul_left_of_neg theorem

(ha : a < 0) : a * b < a * c ↔ c < b

Full source

@[simp high] protected lemma mul_lt_mul_left_of_neg (ha : a < 0) :
    a * b < a * c ↔ c < b := by
  rw [← Int.neg_lt_neg_iff, Int.neg_mul_eq_neg_mul, Int.neg_mul_eq_neg_mul,
    Int.mul_lt_mul_left <| Int.neg_pos.2 ha]

Left Multiplication Reverses Strict Inequality for Negative Integers

Informal description

For any integer $a < 0$ and integers $b, c$, the inequality $a \cdot b < a \cdot c$ holds if and only if $c < b$.

Int.mul_lt_mul_right_of_neg theorem

(ha : a < 0) : b * a < c * a ↔ c < b

Full source

@[simp high] protected lemma mul_lt_mul_right_of_neg (ha : a < 0) :
    b * a < c * a ↔ c < b := by
  rw [← Int.neg_lt_neg_iff, Int.neg_mul_eq_mul_neg, Int.neg_mul_eq_mul_neg,
    Int.mul_lt_mul_right <| Int.neg_pos.2 ha]

Right Multiplication Reverses Strict Inequality for Negative Integers

Informal description

For any integers $a$, $b$, and $c$ with $a < 0$, the inequality $b \cdot a < c \cdot a$ holds if and only if $c < b$.

Int.natAbs_ofNat' theorem

(n : ℕ) : natAbs (ofNat n) = n

Full source

@[simp] lemma natAbs_ofNat' (n : ℕ) : natAbs (ofNat n) = n := rfl

Absolute Value of Natural Number Cast to Integer Equals Original Number

Informal description

For any natural number $n$, the absolute value (as a natural number) of the integer constructed from $n$ is equal to $n$ itself, i.e., $\text{natAbs}(n) = n$.

Int.natAbs_add_of_nonneg theorem

: ∀ {a b : Int}, 0 ≤ a → 0 ≤ b → natAbs (a + b) = natAbs a + natAbs b

Full source

lemma natAbs_add_of_nonneg : ∀ {a b : Int}, 0 ≤ a → 0 ≤ b → natAbs (a + b) = natAbs a + natAbs b
  | ofNat _, ofNat _, _, _ => rfl

Natural Absolute Value of Sum of Nonnegative Integers

Informal description

For any integers $a$ and $b$ such that $0 \leq a$ and $0 \leq b$, the natural absolute value of their sum equals the sum of their natural absolute values, i.e., $\text{natAbs}(a + b) = \text{natAbs}(a) + \text{natAbs}(b)$.

Int.natAbs_add_of_nonpos theorem

{a b : Int} (ha : a ≤ 0) (hb : b ≤ 0) : natAbs (a + b) = natAbs a + natAbs b

Full source

lemma natAbs_add_of_nonpos {a b : Int} (ha : a ≤ 0) (hb : b ≤ 0) :
    natAbs (a + b) = natAbs a + natAbs b := by
  omega

Natural Absolute Value of Sum of Nonpositive Integers

Informal description

For any integers $a$ and $b$ such that $a \leq 0$ and $b \leq 0$, the natural absolute value of their sum equals the sum of their natural absolute values, i.e., $\text{natAbs}(a + b) = \text{natAbs}(a) + \text{natAbs}(b)$.

Int.natAbs_pow theorem

(n : ℤ) (k : ℕ) : Int.natAbs (n ^ k) = Int.natAbs n ^ k

Full source

lemma natAbs_pow (n : ℤ) (k : ℕ) : Int.natAbs (n ^ k) = Int.natAbs n ^ k := by
  induction k with
  | zero => rfl
  | succ k ih => rw [Int.pow_succ, natAbs_mul, Nat.pow_succ, ih, Nat.mul_comm]

Natural Absolute Value Preserves Integer Powers: $\text{natAbs}(n^k) = (\text{natAbs}\,n)^k$

Informal description

For any integer $n$ and natural number $k$, the natural absolute value of $n^k$ is equal to the $k$-th power of the natural absolute value of $n$, i.e., $\text{natAbs}(n^k) = (\text{natAbs}\,n)^k$.

Int.natAbs_sq theorem

(x : ℤ) : (x.natAbs : ℤ) ^ 2 = x ^ 2

Full source

lemma natAbs_sq (x : ℤ) : (x.natAbs : ℤ) ^ 2 = x ^ 2 := by
  simp [Int.pow_succ, Int.pow_zero, Int.natAbs_mul_self']

Square of Natural Absolute Value Equals Square of Integer

Informal description

For any integer $x$, the square of its natural absolute value (as an integer) equals the square of $x$, i.e., $(\text{natAbs}\,x)^2 = x^2$.

Int.sign_mul_self_eq_natAbs theorem

: ∀ a : Int, sign a * a = natAbs a

Full source

theorem sign_mul_self_eq_natAbs : ∀ a : Int, sign a * a = natAbs a
  | 0      => rfl
  | Nat.succ _ => Int.one_mul _
  | -[_+1] => (Int.neg_eq_neg_one_mul _).symm

Sign-Natural Absolute Value Identity: $\text{sign}(a) \cdot a = \text{natAbs}(a)$

Informal description

For any integer $a$, the product of its sign and itself equals its natural absolute value, i.e., $\text{sign}(a) \cdot a = \text{natAbs}(a)$.

Int.natCast_ediv theorem

(m n : ℕ) : ((m / n : ℕ) : ℤ) = m / n

Full source

@[simp, norm_cast] lemma natCast_ediv (m n : ℕ) : ((m / n : ℕ) : ℤ) = m / n := rfl

Integer Division Preserves Natural Division for Casts

Informal description

For any natural numbers $m$ and $n$, the integer division of their casts to integers equals the cast of their natural number division, i.e., $\lfloor m / n \rfloor_{\mathbb{Z}} = \lfloor m / n \rfloor_{\mathbb{N}}$.

Int.natCast_div theorem

(m n : ℕ) : ((m / n : ℕ) : ℤ) = m / n

Full source

lemma natCast_div (m n : ℕ) : ((m / n : ℕ) : ℤ) = m / n := natCast_ediv m n

Natural Division Preserved Under Integer Lift: $(m / n : \mathbb{Z}) = (m : \mathbb{Z}) / (n : \mathbb{Z})$

Informal description

For any natural numbers $m$ and $n$, the integer division of their canonical integer lifts equals the canonical integer lift of their natural number division, i.e., $(m / n : \mathbb{Z}) = (m : \mathbb{Z}) / (n : \mathbb{Z})$.

Int.ediv_of_neg_of_pos theorem

{a b : ℤ} (Ha : a < 0) (Hb : 0 < b) : ediv a b = -((-a - 1) / b + 1)

Full source

lemma ediv_of_neg_of_pos {a b : ℤ} (Ha : a < 0) (Hb : 0 < b) : ediv a b = -((-a - 1) / b + 1) :=
  match a, b, eq_negSucc_of_lt_zero Ha, eq_succ_of_zero_lt Hb with
  | _, _, ⟨m, rfl⟩, ⟨n, rfl⟩ => by
    rw [show (- -[m+1] : ℤ) = (m + 1 : ℤ) by rfl]; rw [Int.add_sub_cancel]; rfl

Integer Division Formula for Negative Dividend and Positive Divisor

Informal description

For any integers $a$ and $b$ such that $a < 0$ and $0 < b$, the integer division of $a$ by $b$ satisfies the equation: \[ a / b = -\left(\frac{-a - 1}{b} + 1\right). \]

Int.natCast_mod theorem

(m n : ℕ) : (↑(m % n) : ℤ) = ↑m % ↑n

Full source

@[simp, norm_cast] lemma natCast_mod (m n : ℕ) : (↑(m % n) : ℤ) = ↑m % ↑n := rfl

Preservation of Modulus Operation under Integer Lift

Informal description

For any natural numbers $m$ and $n$, the canonical integer lift of the modulus operation $m \bmod n$ equals the modulus operation applied to the integer lifts of $m$ and $n$, i.e., $(m \bmod n : \mathbb{Z}) = (m : \mathbb{Z}) \bmod (n : \mathbb{Z})$.

Int.add_emod_eq_add_mod_right theorem

{m n k : ℤ} (i : ℤ) (H : m % n = k % n) : (m + i) % n = (k + i) % n

Full source

lemma add_emod_eq_add_mod_right {m n k : ℤ} (i : ℤ) (H : m % n = k % n) :
    (m + i) % n = (k + i) % n := by rw [← emod_add_emod, ← emod_add_emod k, H]

Modular Arithmetic: Addition Preserves Congruence

Informal description

For any integers $m$, $n$, $k$, and $i$, if $m \bmod n = k \bmod n$, then $(m + i) \bmod n = (k + i) \bmod n$.

Int.neg_emod_two theorem

(i : ℤ) : -i % 2 = i % 2

Full source

@[simp] lemma neg_emod_two (i : ℤ) : -i % 2 = i % 2 := by omega

Modulo Two of Negative Integer Equals Modulo Two of Positive Integer

Informal description

For any integer $i$, the remainder of $-i$ when divided by 2 is equal to the remainder of $i$ when divided by 2, i.e., $-i \bmod 2 = i \bmod 2$.

Int.div_le_iff_of_dvd_of_pos theorem

(hb : 0 < b) (hba : b ∣ a) : a / b ≤ c ↔ a ≤ b * c

Full source

lemma div_le_iff_of_dvd_of_pos (hb : 0 < b) (hba : b ∣ a) : a / b ≤ c ↔ a ≤ b * c := by
  obtain ⟨x, rfl⟩ := hba; simp [*, Int.ne_of_gt]

Division Inequality for Positive Divisors in Integers

Informal description

For integers $a$, $b$, and $c$ with $b > 0$ and $b$ dividing $a$, the inequality $a / b \leq c$ holds if and only if $a \leq b \cdot c$.

Int.div_le_iff_of_dvd_of_neg theorem

(hb : b < 0) (hba : b ∣ a) : a / b ≤ c ↔ b * c ≤ a

Full source

lemma div_le_iff_of_dvd_of_neg (hb : b < 0) (hba : b ∣ a) : a / b ≤ c ↔ b * c ≤ a := by
  obtain ⟨x, rfl⟩ := hba; simp [*, Int.ne_of_lt]

Division Inequality for Negative Divisors in Integers

Informal description

For integers $a$, $b$, and $c$, if $b$ is negative and divides $a$, then the inequality $a / b \leq c$ holds if and only if $b \cdot c \leq a$.

Int.div_lt_iff_of_dvd_of_pos theorem

(hb : 0 < b) (hba : b ∣ a) : a / b < c ↔ a < b * c

Full source

lemma div_lt_iff_of_dvd_of_pos (hb : 0 < b) (hba : b ∣ a) : a / b < c ↔ a < b * c := by
  obtain ⟨x, rfl⟩ := hba; simp [*, Int.ne_of_gt]

Division Inequality for Positive Divisors in Integers

Informal description

For integers $a$, $b$, and $c$, if $b$ is positive and divides $a$, then the inequality $a / b < c$ holds if and only if $a < b \cdot c$.

Int.div_lt_iff_of_dvd_of_neg theorem

(hb : b < 0) (hba : b ∣ a) : a / b < c ↔ b * c < a

Full source

lemma div_lt_iff_of_dvd_of_neg (hb : b < 0) (hba : b ∣ a) : a / b < c ↔ b * c < a := by
  obtain ⟨x, rfl⟩ := hba; simp [*, Int.ne_of_lt]

Division Inequality for Negative Divisors in Integers

Informal description

For integers $a$, $b$, and $c$ with $b < 0$ and $b$ dividing $a$, the inequality $a / b < c$ holds if and only if $b \cdot c < a$.

Int.le_div_iff_of_dvd_of_pos theorem

(hc : 0 < c) (hcb : c ∣ b) : a ≤ b / c ↔ c * a ≤ b

Full source

lemma le_div_iff_of_dvd_of_pos (hc : 0 < c) (hcb : c ∣ b) : a ≤ b / c ↔ c * a ≤ b := by
  obtain ⟨x, rfl⟩ := hcb; simp [*, Int.ne_of_gt]

Integer Division Inequality for Positive Divisors

Informal description

For integers $a$, $b$, and $c$ with $c > 0$ and $c$ dividing $b$, we have $a \leq b / c$ if and only if $c \cdot a \leq b$.

Int.le_div_iff_of_dvd_of_neg theorem

(hc : c < 0) (hcb : c ∣ b) : a ≤ b / c ↔ b ≤ c * a

Full source

lemma le_div_iff_of_dvd_of_neg (hc : c < 0) (hcb : c ∣ b) : a ≤ b / c ↔ b ≤ c * a := by
  obtain ⟨x, rfl⟩ := hcb; simp [*, Int.ne_of_lt]

Division Inequality for Negative Divisors: $a \leq b/c \leftrightarrow b \leq c \cdot a$ when $c < 0$ and $c \mid b$

Informal description

For integers $a$, $b$, and $c$ with $c < 0$ and $c$ dividing $b$, the inequality $a \leq b / c$ holds if and only if $b \leq c \cdot a$.

Int.lt_div_iff_of_dvd_of_pos theorem

(hc : 0 < c) (hcb : c ∣ b) : a < b / c ↔ c * a < b

Full source

lemma lt_div_iff_of_dvd_of_pos (hc : 0 < c) (hcb : c ∣ b) : a < b / c ↔ c * a < b := by
  obtain ⟨x, rfl⟩ := hcb; simp [*, Int.ne_of_gt]

Inequality Relating Integer Division and Multiplication for Positive Divisors

Informal description

For integers $a$, $b$, and $c$ with $c > 0$ and $c$ dividing $b$, we have $a < b / c$ if and only if $c \cdot a < b$.

Int.lt_div_iff_of_dvd_of_neg theorem

(hc : c < 0) (hcb : c ∣ b) : a < b / c ↔ b < c * a

Full source

lemma lt_div_iff_of_dvd_of_neg (hc : c < 0) (hcb : c ∣ b) : a < b / c ↔ b < c * a := by
  obtain ⟨x, rfl⟩ := hcb; simp [*, Int.ne_of_lt]

Inequality Relation for Integer Division by Negative Divisor

Informal description

For integers $a$, $b$, and $c$ with $c < 0$ and $c$ dividing $b$, the inequality $a < b / c$ holds if and only if $b < c \cdot a$.

Int.div_le_div_iff_of_dvd_of_pos_of_pos theorem

(hb : 0 < b) (hd : 0 < d) (hba : b ∣ a) (hdc : d ∣ c) : a / b ≤ c / d ↔ d * a ≤ c * b

Full source

lemma div_le_div_iff_of_dvd_of_pos_of_pos (hb : 0 < b) (hd : 0 < d) (hba : b ∣ a)
    (hdc : d ∣ c) : a / b ≤ c / d ↔ d * a ≤ c * b := by
  obtain ⟨⟨x, rfl⟩, y, rfl⟩ := hba, hdc
  simp [*, Int.ne_of_lt, Int.ne_of_gt, d.mul_assoc, b.mul_comm]

Division Inequality for Positive Divisors in Integers

Informal description

For integers $a, b, c, d$ with $b > 0$, $d > 0$, and where $b$ divides $a$ and $d$ divides $c$, the inequality $\frac{a}{b} \leq \frac{c}{d}$ holds if and only if $d \cdot a \leq c \cdot b$.

Int.div_le_div_iff_of_dvd_of_pos_of_neg theorem

(hb : 0 < b) (hd : d < 0) (hba : b ∣ a) (hdc : d ∣ c) : a / b ≤ c / d ↔ c * b ≤ d * a

Full source

lemma div_le_div_iff_of_dvd_of_pos_of_neg (hb : 0 < b) (hd : d < 0) (hba : b ∣ a) (hdc : d ∣ c) :
    a / b ≤ c / d ↔ c * b ≤ d * a := by
  obtain ⟨⟨x, rfl⟩, y, rfl⟩ := hba, hdc
  simp [*, Int.ne_of_lt, Int.ne_of_gt, d.mul_assoc, b.mul_comm]

Inequality for Integer Division with Mixed Signs and Divisibility Conditions

Informal description

For integers $a, b, c, d$ with $b > 0$, $d < 0$, and where $b$ divides $a$ and $d$ divides $c$, the inequality $\frac{a}{b} \leq \frac{c}{d}$ holds if and only if $c \cdot b \leq d \cdot a$.

Int.div_le_div_iff_of_dvd_of_neg_of_pos theorem

(hb : b < 0) (hd : 0 < d) (hba : b ∣ a) (hdc : d ∣ c) : a / b ≤ c / d ↔ c * b ≤ d * a

Full source

lemma div_le_div_iff_of_dvd_of_neg_of_pos (hb : b < 0) (hd : 0 < d) (hba : b ∣ a)  (hdc : d ∣ c) :
    a / b ≤ c / d ↔ c * b ≤ d * a := by
  obtain ⟨⟨x, rfl⟩, y, rfl⟩ := hba, hdc
  simp [*, Int.ne_of_lt, Int.ne_of_gt, d.mul_assoc, b.mul_comm]

Inequality for Integer Division with Negative and Positive Denominators

Informal description

For integers $a, b, c, d$ with $b < 0$, $d > 0$, and where $b$ divides $a$ and $d$ divides $c$, the inequality $\frac{a}{b} \leq \frac{c}{d}$ holds if and only if $c \cdot b \leq d \cdot a$.

Int.div_le_div_iff_of_dvd_of_neg_of_neg theorem

(hb : b < 0) (hd : d < 0) (hba : b ∣ a) (hdc : d ∣ c) : a / b ≤ c / d ↔ d * a ≤ c * b

Full source

lemma div_le_div_iff_of_dvd_of_neg_of_neg (hb : b < 0) (hd : d < 0) (hba : b ∣ a) (hdc : d ∣ c) :
    a / b ≤ c / d ↔ d * a ≤ c * b := by
  obtain ⟨⟨x, rfl⟩, y, rfl⟩ := hba, hdc
  simp [*, Int.ne_of_lt, Int.ne_of_gt, d.mul_assoc, b.mul_comm]

Inequality for Integer Division with Negative Divisors

Informal description

For integers $a, b, c, d$ with $b < 0$, $d < 0$, and where $b$ divides $a$ and $d$ divides $c$, the inequality $\frac{a}{b} \leq \frac{c}{d}$ holds if and only if $d \cdot a \leq c \cdot b$.

Int.div_lt_div_iff_of_dvd_of_pos theorem

(hb : 0 < b) (hd : 0 < d) (hba : b ∣ a) (hdc : d ∣ c) : a / b < c / d ↔ d * a < c * b

Full source

lemma div_lt_div_iff_of_dvd_of_pos (hb : 0 < b) (hd : 0 < d) (hba : b ∣ a) (hdc : d ∣ c) :
    a / b < c / d ↔ d * a < c * b := by
  obtain ⟨⟨x, rfl⟩, y, rfl⟩ := hba, hdc
  simp [*, Int.ne_of_lt, Int.ne_of_gt, d.mul_assoc, b.mul_comm]

Integer Division Inequality for Positive Divisors: $\frac{a}{b} < \frac{c}{d} \leftrightarrow d \cdot a < c \cdot b$

Informal description

For integers $a, b, c, d$ with $b > 0$, $d > 0$, and where $b$ divides $a$ and $d$ divides $c$, the inequality $\frac{a}{b} < \frac{c}{d}$ holds if and only if $d \cdot a < c \cdot b$.

Int.div_lt_div_iff_of_dvd_of_pos_of_neg theorem

(hb : 0 < b) (hd : d < 0) (hba : b ∣ a) (hdc : d ∣ c) : a / b < c / d ↔ c * b < d * a

Full source

lemma div_lt_div_iff_of_dvd_of_pos_of_neg (hb : 0 < b) (hd : d < 0) (hba : b ∣ a) (hdc : d ∣ c) :
    a / b < c / d ↔ c * b < d * a := by
  obtain ⟨⟨x, rfl⟩, y, rfl⟩ := hba, hdc
  simp [*, Int.ne_of_lt, Int.ne_of_gt, d.mul_assoc, b.mul_comm]

Inequality for Integer Division with Mixed Signs and Divisibility Conditions

Informal description

Let $a, b, c, d$ be integers such that $b > 0$, $d < 0$, $b$ divides $a$, and $d$ divides $c$. Then the inequality $\frac{a}{b} < \frac{c}{d}$ holds if and only if $c \cdot b < d \cdot a$.

Int.div_lt_div_iff_of_dvd_of_neg_of_pos theorem

(hb : b < 0) (hd : 0 < d) (hba : b ∣ a) (hdc : d ∣ c) : a / b < c / d ↔ c * b < d * a

Full source

lemma div_lt_div_iff_of_dvd_of_neg_of_pos (hb : b < 0) (hd : 0 < d) (hba : b ∣ a) (hdc : d ∣ c) :
    a / b < c / d ↔ c * b < d * a := by
  obtain ⟨⟨x, rfl⟩, y, rfl⟩ := hba, hdc
  simp [*, Int.ne_of_lt, Int.ne_of_gt, d.mul_assoc, b.mul_comm]

Inequality of Integer Division with Negative Divisor and Positive Denominator

Informal description

For integers $a, b, c, d$ with $b < 0$, $d > 0$, and where $b$ divides $a$ and $d$ divides $c$, the inequality $\frac{a}{b} < \frac{c}{d}$ holds if and only if $c \cdot b < d \cdot a$.

Int.div_lt_div_iff_of_dvd_of_neg_of_neg theorem

(hb : b < 0) (hd : d < 0) (hba : b ∣ a) (hdc : d ∣ c) : a / b < c / d ↔ d * a < c * b

Full source

lemma div_lt_div_iff_of_dvd_of_neg_of_neg (hb : b < 0) (hd : d < 0) (hba : b ∣ a) (hdc : d ∣ c) :
    a / b < c / d ↔ d * a < c * b := by
  obtain ⟨⟨x, rfl⟩, y, rfl⟩ := hba, hdc
  simp [*, Int.ne_of_lt, Int.ne_of_gt, d.mul_assoc, b.mul_comm]

Inequality of Integer Division with Negative Divisors and Dividends

Informal description

For integers $a, b, c, d$ with $b < 0$, $d < 0$, and where $b$ divides $a$ and $d$ divides $c$, the inequality $\frac{a}{b} < \frac{c}{d}$ holds if and only if $d \cdot a < c \cdot b$.

Int.emod_two_eq_zero_or_one theorem

(n : ℤ) : n % 2 = 0 ∨ n % 2 = 1

Full source

lemma emod_two_eq_zero_or_one (n : ℤ) : n % 2 = 0 ∨ n % 2 = 1 := by omega

Parity of Integers Modulo 2: $n \bmod 2 \in \{0,1\}$

Informal description

For any integer $n$, the remainder when $n$ is divided by 2 is either 0 or 1, i.e., $n \bmod 2 = 0$ or $n \bmod 2 = 1$.

Int.mul_dvd_mul theorem

: a ∣ b → c ∣ d → a * c ∣ b * d

Full source

protected lemma mul_dvd_mul : a ∣ b → c ∣ d → a * c ∣ b * d
  | ⟨e, he⟩, ⟨f, hf⟩ => ⟨e * f, by simp [he, hf, Int.mul_assoc, Int.mul_left_comm, Nat.mul_comm]⟩

Product Divisibility: $a \mid b \land c \mid d \Rightarrow a \cdot c \mid b \cdot d$

Informal description

For any integers $a, b, c, d$, if $a$ divides $b$ and $c$ divides $d$, then the product $a \cdot c$ divides the product $b \cdot d$.

Int.mul_dvd_mul_left theorem

(a : ℤ) (h : b ∣ c) : a * b ∣ a * c

Full source

protected lemma mul_dvd_mul_left (a : ℤ) (h : b ∣ c) : a * b ∣ a * c := Int.mul_dvd_mul a.dvd_refl h

Left Multiplication Preserves Divisibility: $b \mid c \Rightarrow a \cdot b \mid a \cdot c$

Informal description

For any integers $a$, $b$, and $c$, if $b$ divides $c$, then the product $a \cdot b$ divides the product $a \cdot c$.

Int.mul_dvd_mul_right theorem

(a : ℤ) (h : b ∣ c) : b * a ∣ c * a

Full source

protected lemma mul_dvd_mul_right (a : ℤ) (h : b ∣ c) : b * a ∣ c * a :=
  Int.mul_dvd_mul h a.dvd_refl

Right Multiplication Preserves Divisibility: $b \mid c \Rightarrow b \cdot a \mid c \cdot a$

Informal description

For any integers $a$, $b$, and $c$, if $b$ divides $c$, then the product $b \cdot a$ divides the product $c \cdot a$.

Int.dvd_mul_of_div_dvd theorem

(h : b ∣ a) (hdiv : a / b ∣ c) : a ∣ b * c

Full source

lemma dvd_mul_of_div_dvd (h : b ∣ a) (hdiv : a / b ∣ c) : a ∣ b * c := by
  obtain ⟨e, rfl⟩ := hdiv
  rw [← Int.mul_assoc, Int.mul_comm _ (a / b), Int.ediv_mul_cancel h]
  exact Int.dvd_mul_right a e

Divisibility of Product via Quotient: $a \mid b \cdot c$ from $b \mid a$ and $a/b \mid c$

Informal description

For integers $a$, $b$, and $c$, if $b$ divides $a$ and the quotient $a / b$ divides $c$, then $a$ divides the product $b \cdot c$.

Int.div_dvd_iff_dvd_mul theorem

(h : b ∣ a) (hb : b ≠ 0) : a / b ∣ c ↔ a ∣ b * c

Full source

@[simp] lemma div_dvd_iff_dvd_mul (h : b ∣ a) (hb : b ≠ 0) : a / b ∣ ca / b ∣ c ↔ a ∣ b * c :=
  exists_congr <| fun d ↦ by
  have := Int.dvd_trans (Int.dvd_mul_left _ _) (Int.mul_dvd_mul_left d h)
  rw [eq_comm, Int.mul_comm, ← Int.mul_ediv_assoc d h, Int.ediv_eq_iff_eq_mul_right hb this,
    Int.mul_comm, eq_comm]

Quotient Divides iff Dividend Divides Product: $a/b \mid c \leftrightarrow a \mid b \cdot c$ when $b \mid a$ and $b \neq 0$

Informal description

For any integers $a$, $b$, and $c$ with $b \neq 0$, if $b$ divides $a$, then the quotient $a / b$ divides $c$ if and only if $a$ divides the product $b \cdot c$.

Int.mul_dvd_of_dvd_div theorem

(hcb : c ∣ b) (h : a ∣ b / c) : c * a ∣ b

Full source

lemma mul_dvd_of_dvd_div (hcb : c ∣ b) (h : a ∣ b / c) : c * a ∣ b :=
  have ⟨d, hd⟩ := h
  ⟨d, by simpa [Int.mul_comm, Int.mul_left_comm] using Int.eq_mul_of_ediv_eq_left hcb hd⟩

Product Divisibility from Quotient Divisibility: $c \mid b$ and $a \mid (b/c)$ implies $c \cdot a \mid b$

Informal description

For integers $a$, $b$, and $c$, if $c$ divides $b$ and $a$ divides the quotient $b/c$, then the product $c \cdot a$ divides $b$.

Int.dvd_div_of_mul_dvd theorem

(h : a * b ∣ c) : b ∣ c / a

Full source

lemma dvd_div_of_mul_dvd (h : a * b ∣ c) : b ∣ c / a := by
  obtain rfl | ha := Decidable.em (a = 0)
  · simp
  · obtain ⟨d, rfl⟩ := h
    simp [Int.mul_assoc, ha]

Divisibility of Quotient by Factor Implied by Product Divisibility

Informal description

For any integers $a$, $b$, and $c$, if $a \cdot b$ divides $c$, then $b$ divides the quotient $c / a$.

Int.dvd_div_iff_mul_dvd theorem

(hbc : c ∣ b) : a ∣ b / c ↔ c * a ∣ b

Full source

@[simp] lemma dvd_div_iff_mul_dvd (hbc : c ∣ b) : a ∣ b / ca ∣ b / c ↔ c * a ∣ b :=
  ⟨mul_dvd_of_dvd_div hbc, dvd_div_of_mul_dvd⟩

Divisibility of Quotient Equivalent to Product Divisibility: $a \mid (b/c) \leftrightarrow c \cdot a \mid b$

Informal description

For any integers $a$, $b$, and $c$ such that $c$ divides $b$, we have that $a$ divides the quotient $b/c$ if and only if the product $c \cdot a$ divides $b$.

Int.ediv_dvd_ediv theorem

: ∀ {a b c : ℤ}, a ∣ b → b ∣ c → b / a ∣ c / a

Full source

lemma ediv_dvd_ediv : ∀ {a b c : ℤ}, a ∣ b → b ∣ c → b / a ∣ c / a
  | a, _, _, ⟨b, rfl⟩, ⟨c, rfl⟩ =>
    if az : a = 0 then by simp [az]
    else by
      rw [Int.mul_ediv_cancel_left _ az, Int.mul_assoc, Int.mul_ediv_cancel_left _ az]
      apply Int.dvd_mul_right

Divisibility Preservation under Integer Division

Informal description

For any integers $a$, $b$, and $c$, if $a$ divides $b$ and $b$ divides $c$, then the integer division of $b$ by $a$ divides the integer division of $c$ by $a$, i.e., $b/a \mid c/a$.

Int.exists_lt_and_lt_iff_not_dvd theorem

(m : ℤ) (hn : 0 < n) : (∃ k, n * k < m ∧ m < n * (k + 1)) ↔ ¬n ∣ m

Full source

/-- If `n > 0` then `m` is not divisible by `n` iff it is between `n * k` and `n * (k + 1)`
  for some `k`. -/
lemma exists_lt_and_lt_iff_not_dvd (m : ℤ) (hn : 0 < n) :
    (∃ k, n * k < m ∧ m < n * (k + 1)) ↔ ¬n ∣ m := by
  refine ⟨?_, fun h ↦ ?_⟩
  · rintro ⟨k, h1k, h2k⟩ ⟨l, rfl⟩
    replace h1k := lt_of_mul_lt_mul_left h1k (by omega)
    replace h2k := lt_of_mul_lt_mul_left h2k (by omega)
    rw [Int.lt_add_one_iff, ← Int.not_lt] at h2k
    exact h2k h1k
  · rw [dvd_iff_emod_eq_zero, ← Ne] at h
    rw [← emod_add_ediv m n]
    refine ⟨m / n, Int.lt_add_of_pos_left _ ?_, ?_⟩
    · have := emod_nonneg m (Int.ne_of_gt hn)
      omega
    · rw [Int.add_comm _ (1 : ℤ), Int.mul_add, Int.mul_one]
      exact Int.add_lt_add_right (emod_lt_of_pos _ hn) _

Characterization of Non-Divisibility via Integer Intervals

Informal description

For any integers $m$ and $n$ with $n > 0$, the following are equivalent: 1. There exists an integer $k$ such that $n \cdot k < m < n \cdot (k + 1)$. 2. $n$ does not divide $m$.

Int.natAbs_ediv_of_dvd theorem

(a b : ℤ) (H : b ∣ a) : natAbs (a / b) = natAbs a / natAbs b

Full source

lemma natAbs_ediv_of_dvd (a b : ℤ) (H : b ∣ a) : natAbs (a / b) = natAbs a / natAbs b := by
  if h : b = 0 then
    simp_all
  else
    simp [natAbs_ediv, H, h]

Absolute Value Preserves Integer Division under Divisibility

Informal description

For any integers $a$ and $b$ such that $b$ divides $a$, the natural number absolute value of the integer division $a / b$ is equal to the natural number division of the absolute values of $a$ and $b$, i.e., $\text{natAbs}(a / b) = \text{natAbs}(a) / \text{natAbs}(b)$.

Int.dvd_of_mul_dvd_mul_left theorem

(ha : a ≠ 0) (h : a * m ∣ a * n) : m ∣ n

Full source

lemma dvd_of_mul_dvd_mul_left (ha : a ≠ 0) (h : a * m ∣ a * n) : m ∣ n := by
  obtain ⟨b, hb⟩ := h
  rw [Int.mul_assoc, Int.mul_eq_mul_left_iff ha] at hb
  exact ⟨_, hb⟩

Left Cancellation Property for Integer Divisibility

Informal description

For any integers $a$, $m$, and $n$ with $a \neq 0$, if $a \cdot m$ divides $a \cdot n$, then $m$ divides $n$.

Int.dvd_of_mul_dvd_mul_right theorem

(ha : a ≠ 0) (h : m * a ∣ n * a) : m ∣ n

Full source

lemma dvd_of_mul_dvd_mul_right (ha : a ≠ 0) (h : m * a ∣ n * a) : m ∣ n :=
  dvd_of_mul_dvd_mul_left ha (by simpa [Int.mul_comm] using h)

Right Cancellation Property for Integer Divisibility

Informal description

For any integers $a$, $m$, and $n$ with $a \neq 0$, if $m \cdot a$ divides $n \cdot a$, then $m$ divides $n$.

Int.ofNat_add_negSucc_of_ge theorem

{m n : ℕ} (h : n.succ ≤ m) : ofNat m + -[n+1] = ofNat (m - n.succ)

Full source

lemma ofNat_add_negSucc_of_ge {m n : ℕ} (h : n.succ ≤ m) :
    ofNat m + -[n+1] = ofNat (m - n.succ) := by
  rw [negSucc_eq, ofNat_eq_natCast, ofNat_eq_natCast, ← Int.natCast_one, ← Int.natCast_add,
    ← Int.sub_eq_add_neg, ← Int.natCast_sub h]

Integer Sum of Natural Embedding and Negative Successor Equals Difference Embedding

Informal description

For any natural numbers $m$ and $n$ such that $n + 1 \leq m$, the sum of the integer embedding of $m$ and the negative of the successor of $n$ equals the integer embedding of $m - (n + 1)$, i.e., $\text{ofNat}(m) + -[n+1] = \text{ofNat}(m - (n + 1))$.

Int.natAbs_eq_of_dvd_dvd theorem

(hmn : m ∣ n) (hnm : n ∣ m) : natAbs m = natAbs n

Full source

lemma natAbs_eq_of_dvd_dvd (hmn : m ∣ n) (hnm : n ∣ m) : natAbs m = natAbs n :=
  Nat.dvd_antisymm (natAbs_dvd_natAbs.2 hmn) (natAbs_dvd_natAbs.2 hnm)

Equality of Absolute Values for Mutually Divisible Integers

Informal description

For any integers $m$ and $n$, if $m$ divides $n$ and $n$ divides $m$, then the absolute values of $m$ and $n$ (as natural numbers) are equal, i.e., $|m| = |n|$.

Int.ediv_dvd_of_dvd theorem

(hmn : m ∣ n) : n / m ∣ n

Full source

lemma ediv_dvd_of_dvd (hmn : m ∣ n) : n / m ∣ n := by
  obtain rfl | hm := Decidable.em (m = 0)
  · simpa using hmn
  · obtain ⟨a, ha⟩ := hmn
    simp [ha, Int.mul_ediv_cancel_left _ hm, Int.dvd_mul_left]

Divisibility of Quotient: $(m \mid n) \Rightarrow (n/m \mid n)$

Informal description

For any integers $m$ and $n$, if $m$ divides $n$, then the integer division of $n$ by $m$ (denoted $n / m$) also divides $n$.

Int.le_iff_pos_of_dvd theorem

(ha : 0 < a) (hab : a ∣ b) : a ≤ b ↔ 0 < b

Full source

lemma le_iff_pos_of_dvd (ha : 0 < a) (hab : a ∣ b) : a ≤ b ↔ 0 < b :=
  ⟨Int.lt_of_lt_of_le ha, (Int.le_of_dvd · hab)⟩

Positivity and Ordering Condition for Divisors

Informal description

For integers $a$ and $b$ with $a > 0$ and $a$ dividing $b$, we have $a \leq b$ if and only if $b > 0$.

Int.le_add_iff_lt_of_dvd_sub theorem

(ha : 0 < a) (hab : a ∣ c - b) : a + b ≤ c ↔ b < c

Full source

lemma le_add_iff_lt_of_dvd_sub (ha : 0 < a) (hab : a ∣ c - b) : a + b ≤ c ↔ b < c := by
  rw [Int.add_le_iff_le_sub, ← Int.sub_pos, le_iff_pos_of_dvd ha hab]

Inequality Equivalence for Integer Addition with Divisor Condition: $a + b \leq c \leftrightarrow b < c$ when $a > 0$ and $a \mid (c - b)$

Informal description

For any integers $a$, $b$, and $c$ with $a > 0$ and $a$ dividing $c - b$, the inequality $a + b \leq c$ holds if and only if $b < c$.

Int.sign_natCast_of_ne_zero theorem

{n : ℕ} (hn : n ≠ 0) : Int.sign n = 1

Full source

lemma sign_natCast_of_ne_zero {n : ℕ} (hn : n ≠ 0) : Int.sign n = 1 := sign_ofNat_of_nonzero hn

Sign of Nonzero Natural Number Cast to Integer is One

Informal description

For any natural number $n \neq 0$, the sign of the integer $n$ is equal to $1$.

Int.sign_add_eq_of_sign_eq theorem

: ∀ {m n : ℤ}, m.sign = n.sign → (m + n).sign = n.sign

Full source

lemma sign_add_eq_of_sign_eq : ∀ {m n : ℤ}, m.sign = n.sign → (m + n).sign = n.sign := by
  have : (1 : ℤ) ≠ -1 := by decide
  rintro ((_ | m) | m) ((_ | n) | n) <;> simp [this, this.symm] <;> omega

Sign Preservation Under Addition of Integers with Equal Signs

Informal description

For any integers $m$ and $n$, if the signs of $m$ and $n$ are equal, then the sign of their sum $m + n$ is equal to the sign of $n$.

Int.toNat_natCast theorem

(n : ℕ) : toNat ↑n = n

Full source

@[simp] lemma toNat_natCast (n : ℕ) : toNat ↑n = n := rfl

Preservation of Natural Number under Integer Conversion and `toNat`

Informal description

For any natural number $n$, the canonical conversion of $n$ to an integer and then back to a natural number via `toNat` yields $n$ itself, i.e., $\text{toNat}(n) = n$.

Int.toNat_natCast_add_one theorem

{n : ℕ} : ((n : ℤ) + 1).toNat = n + 1

Full source

@[simp] lemma toNat_natCast_add_one {n : ℕ} : ((n : ℤ) + 1).toNat = n + 1 := rfl

Preservation of Successor under Integer-to-Natural Number Map

Informal description

For any natural number $n$, the canonical map from integers to natural numbers applied to $(n + 1)$ (where $n$ is viewed as an integer) equals $n + 1$ as a natural number. In other words, $\text{toNat}(n + 1) = n + 1$.

Int.lt_toNat theorem

{m : ℕ} : m < toNat n ↔ (m : ℤ) < n

Full source

@[simp]
lemma lt_toNat {m : ℕ} : m < toNat n ↔ (m : ℤ) < n := by rw [← Int.not_le, ← Nat.not_le, toNat_le]

Comparison of Natural Number and Integer via toNat: $m < \text{toNat}(n) ↔ m < n$

Informal description

For any natural number $m$ and integer $n$, the inequality $m < \text{toNat}(n)$ holds if and only if the integer $m$ is less than $n$ when viewed as an integer.

Int.lt_of_toNat_lt theorem

{a b : ℤ} (h : toNat a < toNat b) : a < b

Full source

lemma lt_of_toNat_lt {a b : ℤ} (h : toNat a < toNat b) : a < b :=
  (toNat_lt_toNat <| lt_toNat.1 <| Nat.lt_of_le_of_lt (Nat.zero_le _) h).1 h

Comparison of Integers via Natural Number Embedding: $\text{toNat}(a) < \text{toNat}(b) \Rightarrow a < b$

Informal description

For any integers $a$ and $b$, if the natural number corresponding to $a$ is less than the natural number corresponding to $b$, then $a < b$ as integers.

Int.toNat_pred_coe_of_pos theorem

{i : ℤ} (h : 0 < i) : ((i.toNat - 1 : ℕ) : ℤ) = i - 1

Full source

@[simp] lemma toNat_pred_coe_of_pos {i : ℤ} (h : 0 < i) : ((i.toNat - 1 : ℕ) : ℤ) = i - 1 := by
  simp only [lt_toNat, Int.cast_ofNat_Int, h, natCast_pred_of_pos, Int.le_of_lt h, toNat_of_nonneg]

Integer-to-Natural Predecessor Cast Equals Integer Minus One

Informal description

For any positive integer $i$, the integer obtained by casting the predecessor of the natural number corresponding to $i$ (i.e., $\text{toNat}(i) - 1$) is equal to $i - 1$. In symbols: $((\text{toNat}(i) - 1 : ℕ) : ℤ) = i - 1$.

Int.toNat_sub_of_le theorem

{a b : ℤ} (h : b ≤ a) : (toNat (a - b) : ℤ) = a - b

Full source

theorem toNat_sub_of_le {a b : ℤ} (h : b ≤ a) : (toNat (a - b) : ℤ) = a - b :=
  Int.toNat_of_nonneg (Int.sub_nonneg_of_le h)

Embedding of Natural Number Difference Preserves Integer Difference

Informal description

For any integers $a$ and $b$ such that $b \leq a$, the canonical embedding of the natural number corresponding to $a - b$ into the integers equals the integer difference $a - b$. In other words, $\text{toNat}(a - b) = a - b$ when viewed as integers.

Int.toNat_lt'' theorem

{n : ℕ} (hn : n ≠ 0) : m.toNat < n ↔ m < n

Full source

lemma toNat_lt'' {n : ℕ} (hn : n ≠ 0) : m.toNat < n ↔ m < n := by
  rw [← toNat_lt_toNat, toNat_natCast]; omega

`toNat` Preserves Order Relation with Nonzero Natural Numbers

Informal description

For any natural number $n \neq 0$ and any integer $m$, the natural number obtained by applying `toNat` to $m$ is less than $n$ if and only if $m$ is less than $n$. In symbols: $\text{toNat}(m) < n \leftrightarrow m < n$.

Int.natMod definition

(m n : ℤ) : ℕ

Full source

/-- The modulus of an integer by another as a natural. Uses the E-rounding convention. -/
def natMod (m n : ℤ) : ℕ := (m % n).toNat

Natural modulus of integers

Informal description

The function `Int.natMod` takes two integers $m$ and $n$ and returns the modulus of $m$ by $n$ as a natural number, using the Euclidean rounding convention. Specifically, it computes $m \mod n$ and converts the result to a natural number.

Int.natMod_lt theorem

{n : ℕ} (hn : n ≠ 0) : m.natMod n < n

Full source

lemma natMod_lt {n : ℕ} (hn : n ≠ 0) : m.natMod n < n :=
  (toNat_lt'' hn).2 <| emod_lt_of_pos _ <| by omega

Natural Modulus Bounds: $m \mod_{\mathbb{N}} n < n$ for $n \neq 0$

Informal description

For any nonzero natural number $n$, the natural modulus of an integer $m$ by $n$ is strictly less than $n$, i.e., $m \mod_{\mathbb{N}} n < n$.

Int.pow_eq theorem

(m : ℤ) (n : ℕ) : m.pow n = m ^ n

Full source

/-- For use in `Mathlib.Tactic.NormNum.Pow` -/
@[simp] lemma pow_eq (m : ℤ) (n : ℕ) : m.pow n = m ^ n := rfl

Integer Power Equivalence: $m^{[n]} = m^n$

Informal description

For any integer $m$ and natural number $n$, the $n$-th power of $m$ computed via the `pow` function equals $m$ raised to the power of $n$, i.e., $m^{[n]} = m^n$.