Init.Data.Int.LemmasAux

Int.natCast_le_zero theorem

: {n : Nat} → (n : Int) ≤ 0 ↔ n = 0

Full source

@[simp] theorem natCast_le_zero : {n : Nat} → (n : Int) ≤ 0 ↔ n = 0 := by omega

Natural Number Cast to Integer is Nonpositive if and only if Zero

Informal description

For any natural number $n$, the integer obtained by casting $n$ is less than or equal to zero if and only if $n$ equals zero. In other words, $(n : \mathbb{Z}) \leq 0 \leftrightarrow n = 0$.

Int.sub_eq_iff_eq_add theorem

{b a c : Int} : a - b = c ↔ a = c + b

Full source

protected theorem sub_eq_iff_eq_add {b a c : Int} : a - b = c ↔ a = c + b := by omega

Subtraction-Additive Equivalence: $a - b = c \leftrightarrow a = c + b$

Informal description

For any integers $a$, $b$, and $c$, the equation $a - b = c$ holds if and only if $a = c + b$.

Int.sub_eq_iff_eq_add' theorem

{b a c : Int} : a - b = c ↔ a = b + c

Full source

protected theorem sub_eq_iff_eq_add' {b a c : Int} : a - b = c ↔ a = b + c := by omega

Subtraction Equivalence: $a - b = c \leftrightarrow a = b + c$

Informal description

For any integers $a$, $b$, and $c$, the difference $a - b$ equals $c$ if and only if $a$ equals the sum $b + c$. In other words, $a - b = c \leftrightarrow a = b + c$.

Int.neg_nonpos_iff theorem

(i : Int) : -i ≤ 0 ↔ 0 ≤ i

Full source

@[simp] protected theorem neg_nonpos_iff (i : Int) : -i ≤ 0 ↔ 0 ≤ i := by omega

Negation Nonpositive iff Nonnegative

Informal description

For any integer $i$, the negation of $i$ is less than or equal to zero if and only if $i$ is greater than or equal to zero, i.e., $-i \leq 0 \leftrightarrow 0 \leq i$.

Int.zero_le_ofNat theorem

(n : Nat) : 0 ≤ ((no_index (OfNat.ofNat n)) : Int)

Full source

@[simp] theorem zero_le_ofNat (n : Nat) : 0 ≤ ((no_index (OfNat.ofNat n)) : Int) :=
  ofNat_nonneg _

Nonnegativity of Natural Numbers as Integers

Informal description

For any natural number $n$, the integer obtained by interpreting $n$ as an integer is nonnegative, i.e., $0 \leq n$ where $n$ is viewed as an integer.

Int.neg_natCast_le_natCast theorem

(n m : Nat) : -(n : Int) ≤ (m : Int)

Full source

@[simp] theorem neg_natCast_le_natCast (n m : Nat) : -(n : Int) ≤ (m : Int) :=
  Int.le_trans (by simp) (ofNat_zero_le m)

Negation of Natural Number as Integer is Bounded by Another Natural Number as Integer: $-n \leq m$

Informal description

For any natural numbers $n$ and $m$, the negation of the integer representation of $n$ is less than or equal to the integer representation of $m$, i.e., $-n \leq m$ where $n$ and $m$ are interpreted as integers.

Int.neg_natCast_le_ofNat theorem

(n m : Nat) : -(n : Int) ≤ (no_index (OfNat.ofNat m))

Full source

@[simp] theorem neg_natCast_le_ofNat (n m : Nat) : -(n : Int) ≤ (no_index (OfNat.ofNat m)) :=
  Int.le_trans (by simp) (ofNat_zero_le m)

Negation of Natural Number as Integer is Bounded by Another Natural Number as Integer: $-n \leq m$

Informal description

For any natural numbers $n$ and $m$, the negation of the integer representation of $n$ is less than or equal to the integer representation of $m$, i.e., $-n \leq m$.

Int.neg_ofNat_le_ofNat theorem

(n m : Nat) : -(no_index (OfNat.ofNat n)) ≤ (no_index (OfNat.ofNat m))

Full source

@[simp] theorem neg_ofNat_le_ofNat (n m : Nat) : -(no_index (OfNat.ofNat n)) ≤ (no_index (OfNat.ofNat m)) :=
  Int.le_trans (by simp) (ofNat_zero_le m)

Negation of Natural Number as Integer is Bounded by Another Natural Number as Integer: $-n \leq m$

Informal description

For any natural numbers $n$ and $m$, the negation of the integer representation of $n$ is less than or equal to the integer representation of $m$, i.e., $-n \leq m$ where $n$ and $m$ are interpreted as integers.

Int.neg_ofNat_le_natCast theorem

(n m : Nat) : -(no_index (OfNat.ofNat n)) ≤ (m : Int)

Full source

@[simp] theorem neg_ofNat_le_natCast (n m : Nat) : -(no_index (OfNat.ofNat n)) ≤ (m : Int) :=
  Int.le_trans (by simp) (ofNat_zero_le m)

Negation of Natural Number as Integer is Bounded by Another Natural Number as Integer: $-n \leq m$

Informal description

For any natural numbers $n$ and $m$, the negation of the integer representation of $n$ is less than or equal to the integer representation of $m$, i.e., $-n \leq m$ where $n$ and $m$ are interpreted as integers.

Int.neg_lt_self_iff theorem

{n : Int} : -n < n ↔ 0 < n

Full source

theorem neg_lt_self_iff {n : Int} : -n < n ↔ 0 < n := by
  omega

Negation Inequality: $-n < n \leftrightarrow 0 < n$

Informal description

For any integer $n$, the inequality $-n < n$ holds if and only if $0 < n$.

Int.toNat_sub' theorem

(a : Int) (b : Nat) : (a - b).toNat = a.toNat - b

Full source

@[simp] theorem toNat_sub' (a : Int) (b : Nat) : (a - b).toNat = a.toNat - b := by
  symm
  simp only [Int.toNat]
  split <;> rename_i x a
  · simp only [Int.ofNat_eq_coe]
    split <;> rename_i y b h
    · simp at h
      omega
    · simp [Int.negSucc_eq] at h
      omega
  · simp only [Nat.zero_sub]
    split <;> rename_i y b h
    · simp [Int.negSucc_eq] at h
      omega
    · rfl

Natural number conversion of integer subtraction: $(a - b).\text{toNat} = a.\text{toNat} - b$

Informal description

For any integer $a$ and natural number $b$, the conversion to natural number of the difference $a - b$ equals the truncated subtraction of the natural number conversion of $a$ and $b$, i.e., $(a - b).\text{toNat} = a.\text{toNat} - b$.

Int.toNat_sub_max_self theorem

(a : Int) : (a - max a 0).toNat = 0

Full source

@[simp] theorem toNat_sub_max_self (a : Int) : (a - max a 0).toNat = 0 := by
  simp [toNat]
  split <;> simp_all <;> omega

Natural conversion of $a - \max(a,0)$ equals zero

Informal description

For any integer $a$, the natural number obtained by converting the integer $a - \max(a, 0)$ to a natural number is equal to $0$.

Int.toNat_sub_self_max theorem

(a : Int) : (a - max 0 a).toNat = 0

Full source

@[simp] theorem toNat_sub_self_max (a : Int) : (a - max 0 a).toNat = 0 := by
  simp [toNat]
  split <;> simp_all <;> omega

Natural Conversion of $a - \max(0, a)$ is Zero

Informal description

For any integer $a$, the natural number obtained by converting the integer $a - \max(0, a)$ to a natural number is equal to $0$.

Int.toNat_eq_zero theorem

: ∀ {n : Int}, n.toNat = 0 ↔ n ≤ 0

Full source

@[simp] theorem toNat_eq_zero : ∀ {n : Int}, n.toNat = 0 ↔ n ≤ 0 := by omega

Natural Conversion of Integer to Zero iff Non-Positive

Informal description

For any integer $n$, the natural number conversion of $n$ equals zero if and only if $n$ is less than or equal to zero, i.e., $n \leq 0$.

Int.toNat_le theorem

{m : Int} {n : Nat} : m.toNat ≤ n ↔ m ≤ n

Full source

@[simp] theorem toNat_le {m : Int} {n : Nat} : m.toNat ≤ n ↔ m ≤ n := by omega

Natural Conversion Preserves Order: $m.toNat \leq n \leftrightarrow m \leq n$

Informal description

For any integer $m$ and natural number $n$, the natural number conversion of $m$ (denoted $m.toNat$) satisfies $m.toNat \leq n$ if and only if $m \leq n$.

Int.toNat_lt' theorem

{m : Int} {n : Nat} (hn : 0 < n) : m.toNat < n ↔ m < n

Full source

@[simp] theorem toNat_lt' {m : Int} {n : Nat} (hn : 0 < n) : m.toNat < n ↔ m < n := by omega

Integer to Natural Conversion Preserves Strict Order for Positive $n$

Informal description

For any integer $m$ and natural number $n > 0$, the natural number conversion of $m$ is less than $n$ if and only if $m$ is less than $n$. In other words, $m.toNat < n \leftrightarrow m < n$.

Int.pos_iff_toNat_pos theorem

{n : Int} : 0 < n ↔ 0 < n.toNat

Full source

theorem pos_iff_toNat_pos {n : Int} : 0 < n ↔ 0 < n.toNat := by
  omega

Positivity Criterion for Integers via Natural Conversion

Informal description

For any integer $n$, the statement $0 < n$ holds if and only if $0 < n.\mathrm{toNat}$, where $\mathrm{toNat}$ is the function that converts non-negative integers to natural numbers and maps negative integers to zero.

Int.ofNat_toNat_eq_self theorem

{a : Int} : a.toNat = a ↔ 0 ≤ a

Full source

theorem ofNat_toNat_eq_self {a : Int} : a.toNat = a ↔ 0 ≤ a := by omega

Natural Conversion Equals Self iff Non-Negative

Informal description

For any integer $a$, the natural number conversion of $a$ equals $a$ if and only if $a$ is non-negative, i.e., $a.\mathrm{toNat} = a \leftrightarrow 0 \leq a$.

Int.toNat_le_toNat theorem

{n m : Int} (h : n ≤ m) : n.toNat ≤ m.toNat

Full source

theorem toNat_le_toNat {n m : Int} (h : n ≤ m) : n.toNat ≤ m.toNat := by omega

Monotonicity of Integer to Natural Number Conversion with Respect to Order

Informal description

For any integers $n$ and $m$ such that $n \leq m$, the natural number conversion satisfies $n.\text{toNat} \leq m.\text{toNat}$.

Int.toNat_lt_toNat theorem

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

Full source

theorem toNat_lt_toNat {n m : Int} (hn : 0 < m) : n.toNat < m.toNat ↔ n < m := by omega

Comparison of Natural Conversions: $n.toNat < m.toNat \leftrightarrow n < m$ for $m > 0$

Informal description

For any integers $n$ and $m$ with $m > 0$, the natural number conversion satisfies $n.toNat < m.toNat$ if and only if $n < m$.

Int.min_assoc theorem

: ∀ (a b c : Int), min (min a b) c = min a (min b c)

Full source

@[simp] protected theorem min_assoc : ∀ (a b c : Int), min (min a b) c = min a (min b c) := by omega

Associativity of Minimum Operation on Integers

Informal description

For any integers $a$, $b$, and $c$, the minimum operation satisfies the associativity property: $$\min(\min(a, b), c) = \min(a, \min(b, c))$$

Int.instAssociativeNatMin instance

: Std.Associative (α := Nat) min

Full source

instance : Std.Associative (α := Nat) min := ⟨Nat.min_assoc⟩

Associativity of Minimum on Natural Numbers

Informal description

The minimum operation $\min$ on natural numbers is associative.

Int.min_self_assoc theorem

{m n : Int} : min m (min m n) = min m n

Full source

@[simp] protected theorem min_self_assoc {m n : Int} : min m (min m n) = min m n := by
  rw [← Int.min_assoc, Int.min_self]

Idempotence of Minimum Operation: $\min(m, \min(m, n)) = \min(m, n)$

Informal description

For any integers $m$ and $n$, the minimum of $m$ and the minimum of $m$ and $n$ is equal to the minimum of $m$ and $n$, i.e., $\min(m, \min(m, n)) = \min(m, n)$.

Int.min_self_assoc' theorem

{m n : Int} : min n (min m n) = min n m

Full source

@[simp] protected theorem min_self_assoc' {m n : Int} : min n (min m n) = min n m := by
  rw [Int.min_comm m n, ← Int.min_assoc, Int.min_self]

Self-Associativity of Minimum Operation on Integers: $\min(n, \min(m, n)) = \min(n, m)$

Informal description

For any integers $m$ and $n$, the minimum of $n$ and the minimum of $m$ and $n$ is equal to the minimum of $n$ and $m$, i.e., $$\min(n, \min(m, n)) = \min(n, m).$$

Int.max_assoc theorem

(a b c : Int) : max (max a b) c = max a (max b c)

Full source

@[simp] protected theorem max_assoc (a b c : Int) : max (max a b) c = max a (max b c) := by omega

Associativity of Maximum Operation on Integers: $\max(\max(a, b), c) = \max(a, \max(b, c))$

Informal description

For any integers $a$, $b$, and $c$, the maximum operation satisfies the associativity property: \[ \max(\max(a, b), c) = \max(a, \max(b, c)). \]

Int.instAssociativeNatMax instance

: Std.Associative (α := Nat) max

Full source

instance : Std.Associative (α := Nat) max := ⟨Nat.max_assoc⟩

Associativity of Maximum Operation on Natural Numbers

Informal description

The maximum operation $\max$ on natural numbers is associative.

Int.max_self_assoc theorem

{m n : Int} : max m (max m n) = max m n

Full source

@[simp] protected theorem max_self_assoc {m n : Int} : max m (max m n) = max m n := by
  rw [← Int.max_assoc, Int.max_self]

Idempotence of Maximum Operation with Itself: $\max(m, \max(m, n)) = \max(m, n)$

Informal description

For any integers $m$ and $n$, the maximum of $m$ and the maximum of $m$ and $n$ equals the maximum of $m$ and $n$, i.e., \[ \max(m, \max(m, n)) = \max(m, n). \]

Int.max_self_assoc' theorem

{m n : Int} : max n (max m n) = max n m

Full source

@[simp] protected theorem max_self_assoc' {m n : Int} : max n (max m n) = max n m := by
  rw [Int.max_comm m n, ← Int.max_assoc, Int.max_self]

Associative Property of Maximum with Self: $\max(n, \max(m, n)) = \max(n, m)$

Informal description

For any integers $m$ and $n$, the maximum of $n$ and the maximum of $m$ and $n$ is equal to the maximum of $n$ and $m$, i.e., \[ \max(n, \max(m, n)) = \max(n, m). \]

Int.max_min_distrib_left theorem

(a b c : Int) : max a (min b c) = min (max a b) (max a c)

Full source

protected theorem max_min_distrib_left (a b c : Int) : max a (min b c) = min (max a b) (max a c) := by omega

Left Distributivity of Maximum over Minimum for Integers

Informal description

For any integers $a$, $b$, and $c$, the maximum of $a$ and the minimum of $b$ and $c$ is equal to the minimum of the maximum of $a$ and $b$ and the maximum of $a$ and $c$. In symbols: \[ \max(a, \min(b, c)) = \min(\max(a, b), \max(a, c)) \]

Int.min_max_distrib_left theorem

(a b c : Int) : min a (max b c) = max (min a b) (min a c)

Full source

protected theorem min_max_distrib_left (a b c : Int) : min a (max b c) = max (min a b) (min a c) := by omega

Distributivity of Minimum over Maximum for Integers

Informal description

For any integers $a$, $b$, and $c$, the minimum of $a$ and the maximum of $b$ and $c$ is equal to the maximum of the minimum of $a$ and $b$ and the minimum of $a$ and $c$. In symbols: $$\min(a, \max(b, c)) = \max(\min(a, b), \min(a, c))$$

Int.max_min_distrib_right theorem

(a b c : Int) : max (min a b) c = min (max a c) (max b c)

Full source

protected theorem max_min_distrib_right (a b c : Int) :
    max (min a b) c = min (max a c) (max b c) := by omega

Distributivity of Maximum over Minimum for Integers

Informal description

For any integers $a$, $b$, and $c$, the following distributive law holds: \[ \max(\min(a, b), c) = \min(\max(a, c), \max(b, c)). \]

Int.min_max_distrib_right theorem

(a b c : Int) : min (max a b) c = max (min a c) (min b c)

Full source

protected theorem min_max_distrib_right (a b c : Int) :
    min (max a b) c = max (min a c) (min b c) := by omega

Distributivity of Minimum over Maximum for Integers

Informal description

For any integers $a$, $b$, and $c$, the minimum of the maximum of $a$ and $b$ with $c$ is equal to the maximum of the minimum of $a$ and $c$ with the minimum of $b$ and $c$. In symbols: \[ \min(\max(a, b), c) = \max(\min(a, c), \min(b, c)) \]

Int.sub_min_sub_right theorem

(a b c : Int) : min (a - c) (b - c) = min a b - c

Full source

protected theorem sub_min_sub_right (a b c : Int) : min (a - c) (b - c) = min a b - c := by omega

Minus Distributes Over Min: $\min(a - c, b - c) = \min(a, b) - c$

Informal description

For any integers $a$, $b$, and $c$, the minimum of $(a - c)$ and $(b - c)$ is equal to the minimum of $a$ and $b$ minus $c$, i.e., $\min(a - c, b - c) = \min(a, b) - c$.

Int.sub_max_sub_right theorem

(a b c : Int) : max (a - c) (b - c) = max a b - c

Full source

protected theorem sub_max_sub_right (a b c : Int) : max (a - c) (b - c) = max a b - c := by omega

Max Preserves Subtraction on the Right: $\max(a - c, b - c) = \max(a, b) - c$

Informal description

For any integers $a$, $b$, and $c$, the maximum of the differences $a - c$ and $b - c$ is equal to the difference of the maximum of $a$ and $b$ minus $c$, i.e., \[ \max(a - c, b - c) = \max(a, b) - c. \]

Int.sub_min_sub_left theorem

(a b c : Int) : min (a - b) (a - c) = a - max b c

Full source

protected theorem sub_min_sub_left (a b c : Int) : min (a - b) (a - c) = a - max b c := by omega

Minus-Min Equals Minus-Max Identity for Integers

Informal description

For any integers $a, b, c$, the minimum of the differences $a - b$ and $a - c$ equals the difference between $a$ and the maximum of $b$ and $c$, i.e., $$\min(a - b, a - c) = a - \max(b, c).$$

Int.sub_max_sub_left theorem

(a b c : Int) : max (a - b) (a - c) = a - min b c

Full source

protected theorem sub_max_sub_left (a b c : Int) : max (a - b) (a - c) = a - min b c := by omega

Maximum of Differences Equals Difference with Minimum

Informal description

For any integers $a, b, c$, the maximum of $(a - b)$ and $(a - c)$ equals $a$ minus the minimum of $b$ and $c$, i.e., $$\max(a - b, a - c) = a - \min(b, c).$$

Int.bmod_neg_iff theorem

 {m : Nat} {x : Int} (h2 : -m ≤ x) (h1 : x < m) : (x.bmod m) < 0 ↔ (-(m / 2) ≤ x ∧ x < 0) ∨ ((m + 1) / 2 ≤ x)

Full source

theorem bmod_neg_iff {m : Nat} {x : Int} (h2 : -m ≤ x) (h1 : x < m) :
    (x.bmod m) < 0 ↔ (-(m / 2) ≤ x ∧ x < 0) ∨ ((m + 1) / 2 ≤ x) := by
  simp only [Int.bmod_def]
  by_cases xpos : 0 ≤ x
  · rw [Int.emod_eq_of_lt xpos (by omega)]; omega
  · rw [Int.add_emod_self.symm, Int.emod_eq_of_lt (by omega) (by omega)]; omega

Negativity Condition for Balanced Modulus: $\text{bmod}(x, m) < 0 \iff \left(-\frac{m}{2} \leq x < 0\right) \lor \left(\frac{m+1}{2} \leq x\right)$

Informal description

For any integer $x$ and natural number $m$ such that $-m \leq x < m$, the balanced modulus $x \bmod m$ is negative if and only if either: 1. $-m/2 \leq x < 0$, or 2. $(m + 1)/2 \leq x$.

Int.bmod_eq_self_of_le theorem

{n : Int} {m : Nat} (hn' : -(m / 2) ≤ n) (hn : n < (m + 1) / 2) : n.bmod m = n

Full source

theorem bmod_eq_self_of_le {n : Int} {m : Nat} (hn' : -(m / 2) ≤ n) (hn : n < (m + 1) / 2) :
    n.bmod m = n := by
  rw [← Int.sub_eq_zero]
  have := le_bmod (x := n) (m := m) (by omega)
  have := bmod_lt (x := n) (m := m) (by omega)
  apply eq_zero_of_dvd_of_natAbs_lt_natAbs Int.dvd_bmod_sub_self
  omega

Balanced Modulus Identity for Integers in Symmetric Range: $\text{bmod}(n, m) = n$ when $-\lfloor m/2 \rfloor \leq n < \frac{m+1}{2}$

Informal description

For any integer $n$ and natural number $m$, if $n$ satisfies $-\lfloor m/2 \rfloor \leq n < \frac{m+1}{2}$, then the balanced modulus of $n$ with respect to $m$ equals $n$ itself, i.e., $\text{bmod}(n, m) = n$.

Int.bmod_bmod_of_dvd theorem

{a : Int} {n m : Nat} (hnm : n ∣ m) : (a.bmod m).bmod n = a.bmod n

Full source

theorem bmod_bmod_of_dvd {a : Int} {n m : Nat} (hnm : n ∣ m) :
    (a.bmod m).bmod n = a.bmod n := by
  rw [← Int.sub_eq_iff_eq_add.2 (bmod_add_bdiv a m).symm]
  obtain ⟨k, rfl⟩ := hnm
  simp [Int.mul_assoc]

Nested Balanced Modulus Property under Divisibility: $\text{bmod}(\text{bmod}(a, m), n) = \text{bmod}(a, n)$ when $n \mid m$

Informal description

For any integer $a$ and natural numbers $n$ and $m$ such that $n$ divides $m$, the balanced modulus of the balanced modulus of $a$ with respect to $m$ with respect to $n$ equals the balanced modulus of $a$ with respect to $n$, i.e., \[ \text{bmod}(\text{bmod}(a, m), n) = \text{bmod}(a, n). \]