Basic operations on the integers

This file contains some basic lemmas about integers.

See note [foundational algebra order theory].

TODO

Split this file into:

• Data.Int.Init (or maybe Data.Int.Batteries?) for lemmas that could go to Batteries
• Data.Int.Basic for the lemmas that require mathlib definitions

theorem Int.le_rfl {a : ℤ} : a ≤ a

theorem Int.lt_or_lt_of_ne {a b : ℤ} : a ≠ b → a < b ∨ b < a

theorem Int.lt_or_le (a b : ℤ) : a < b ∨ b ≤ a

theorem Int.le_or_lt (a b : ℤ) : a ≤ b ∨ b < a

theorem Int.lt_asymm {a b : ℤ} : a < b → ¬b < a

theorem Int.le_of_eq {a b : ℤ} (hab : a = b) : a ≤ b

theorem Int.ge_of_eq {a b : ℤ} (hab : a = b) : b ≤ a

theorem Int.le_antisymm_iff {a b : ℤ} : a = b ↔ a ≤ b ∧ b ≤ a

theorem Int.le_iff_eq_or_lt {a b : ℤ} : a ≤ b ↔ a = b ∨ a < b

theorem Int.le_iff_lt_or_eq {a b : ℤ} : a ≤ b ↔ a < b ∨ a = b

theorem Int.one_pos : 0 < 1

theorem Int.one_ne_zero : 1 ≠ 0

theorem Int.one_nonneg : 0 ≤ 1

theorem Int.zero_le_ofNat (n : ℕ) : 0 ≤ ofNat n

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

@[simp]

theorem Int.neg_pos {a : ℤ} : 0 < -a ↔ a < 0

@[simp]

theorem Int.neg_nonneg {a : ℤ} : 0 ≤ -a ↔ a ≤ 0

@[simp]

theorem Int.neg_neg_iff_pos {a : ℤ} : -a < 0 ↔ 0 < a

@[simp]

theorem Int.neg_nonpos_iff_nonneg {a : ℤ} : -a ≤ 0 ↔ 0 ≤ a

@[simp]

theorem Int.sub_pos {a b : ℤ} : 0 < a - b ↔ b < a

@[simp]

theorem Int.sub_nonneg {a b : ℤ} : 0 ≤ a - b ↔ b ≤ a

instance Int.instNontrivial : Nontrivial ℤ

theorem Int.ofNat_add_out (m n : ℕ) : ↑m + ↑n = ↑(m + n)

theorem Int.ofNat_mul_out (m n : ℕ) : ↑m * ↑n = ↑(m * n)

theorem Int.ofNat_add_one_out (n : ℕ) : ↑n + 1 = ↑n.succ

@[simp]

theorem Int.ofNat_injective : Function.Injective ofNat

@[simp]

theorem Int.ofNat_eq_natCast (n : ℕ) : ofNat n = ↑n

theorem Int.natCast_inj {m n : ℕ} : ↑m = ↑n ↔ m = n

@[simp]

theorem Int.natAbs_cast (n : ℕ) : (↑n).natAbs = n

theorem Int.natCast_sub {n m : ℕ} : n ≤ m → ↑(m - n) = ↑m - ↑n

@[simp]

theorem Int.natCast_eq_zero {n : ℕ} : ↑n = 0 ↔ n = 0

theorem Int.natCast_ne_zero {n : ℕ} : ↑n ≠ 0 ↔ n ≠ 0

theorem Int.natCast_ne_zero_iff_pos {n : ℕ} : ↑n ≠ 0 ↔ 0 < n

@[simp]

theorem Int.natCast_pos {n : ℕ} : 0 < ↑n ↔ 0 < n

theorem Int.natCast_succ_pos (n : ℕ) : 0 < ↑n.succ

@[simp]

theorem Int.natCast_nonpos_iff {n : ℕ} : ↑n ≤ 0 ↔ n = 0

theorem Int.natCast_nonneg (n : ℕ) : 0 ≤ ↑n

@[simp]

theorem Int.sign_natCast_add_one (n : ℕ) : (↑n + 1).sign = 1

@[simp]

theorem Int.cast_id {n : ℤ} : ↑n = n

theorem Int.two_mul (n : ℤ) : 2 * n = n + n

theorem Int.mul_le_mul_iff_of_pos_right {a b c : ℤ} (ha : 0 < a) : b * a ≤ c * a ↔ b ≤ c

theorem Int.mul_nonneg_iff_of_pos_right {a b : ℤ} (hb : 0 < b) : 0 ≤ a * b ↔ 0 ≤ a

succ and pred

def Int.succ (a : ℤ) : ℤ

Immediate successor of an integer: succ n = n + 1

Equations

• a.succ = a + 1

def Int.pred (a : ℤ) : ℤ

Immediate predecessor of an integer: pred n = n - 1

Equations

• a.pred = a - 1

theorem Int.natCast_succ (n : ℕ) : ↑n.succ = (↑n).succ

theorem Int.pred_succ (a : ℤ) : a.succ.pred = a

theorem Int.succ_pred (a : ℤ) : a.pred.succ = a

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

theorem Int.succ_neg_succ (a : ℤ) : (-a.succ).succ = -a

theorem Int.neg_pred (a : ℤ) : -a.pred = (-a).succ

theorem Int.pred_neg_pred (a : ℤ) : (-a.pred).pred = -a

theorem Int.pred_nat_succ (n : ℕ) : (↑n.succ).pred = ↑n

theorem Int.neg_nat_succ (n : ℕ) : -↑n.succ = (-↑n).pred

theorem Int.succ_neg_natCast_succ (n : ℕ) : (-↑n.succ).succ = -↑n

theorem Int.natCast_pred_of_pos {n : ℕ} (h : 0 < n) : ↑(n - 1) = ↑n - 1

theorem Int.lt_succ_self (a : ℤ) : a < a.succ

theorem Int.pred_self_lt (a : ℤ) : a.pred < a

theorem Int.le_add_one_iff {m n : ℤ} : m ≤ n + 1 ↔ m ≤ n ∨ m = n + 1

theorem Int.sub_one_lt_iff {m n : ℤ} : m - 1 < n ↔ m ≤ n

theorem Int.le_sub_one_iff {m n : ℤ} : m ≤ n - 1 ↔ m < n

The following few lemmas are proved in the core implementation of the omega tactic. We expose them here with nice user-facing names.

theorem Int.add_le_iff_le_sub {a b c : ℤ} : a + b ≤ c ↔ a ≤ c - b

theorem Int.le_add_iff_sub_le {a b c : ℤ} : a ≤ b + c ↔ a - c ≤ b

theorem Int.add_le_zero_iff_le_neg {a b : ℤ} : a + b ≤ 0 ↔ a ≤ -b

theorem Int.add_le_zero_iff_le_neg' {a b : ℤ} : a + b ≤ 0 ↔ b ≤ -a

theorem Int.add_nonnneg_iff_neg_le {a b : ℤ} : 0 ≤ a + b ↔ -b ≤ a

theorem Int.add_nonnneg_iff_neg_le' {a b : ℤ} : 0 ≤ a + b ↔ -a ≤ b

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

def Int.inductionOn' {C : ℤ → Sort u_1} (z b : ℤ) (H0 : C b) (Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)) (Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)) : C z

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.

Equations

• z.inductionOn' b H0 Hs Hp = cast ⋯ (match z - b with | Int.ofNat n => Int.inductionOn'.pos b H0 Hs n | Int.negSucc n => Int.inductionOn'.neg b H0 Hp n)

def Int.inductionOn'.pos {C : ℤ → Sort u_1} (b : ℤ) (H0 : C b) (Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)) (n : ℕ) : C (b + ↑n)

The positive case of Int.inductionOn'.

Equations

• Int.inductionOn'.pos b H0 Hs 0 = cast ⋯ H0
• Int.inductionOn'.pos b H0 Hs n.succ = cast ⋯ (Hs (b + ↑n) ⋯ (Int.inductionOn'.pos b H0 Hs n))

def Int.inductionOn'.neg {C : ℤ → Sort u_1} (b : ℤ) (H0 : C b) (Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)) (n : ℕ) : C (b + negSucc n)

The negative case of Int.inductionOn'.

Equations

• Int.inductionOn'.neg b H0 Hp 0 = Hp b ⋯ H0
• Int.inductionOn'.neg b H0 Hp n.succ = cast ⋯ (Hp (b + Int.negSucc n) ⋯ (Int.inductionOn'.neg b H0 Hp n))

theorem Int.inductionOn'_self {C : ℤ → Sort u_1} {b : ℤ} {H0 : C b} {Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)} {Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)} : b.inductionOn' b H0 Hs Hp = H0

theorem Int.inductionOn'_add_one {C : ℤ → Sort u_1} {z b : ℤ} {H0 : C b} {Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)} {Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)} (hz : b ≤ z) : (z + 1).inductionOn' b H0 Hs Hp = Hs z hz (z.inductionOn' b H0 Hs Hp)

theorem Int.inductionOn'_sub_one {C : ℤ → Sort u_1} {z b : ℤ} {H0 : C b} {Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)} {Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)} (hz : z ≤ b) : (z - 1).inductionOn' b H0 Hs Hp = Hp z hz (z.inductionOn' b H0 Hs Hp)

def Int.negInduction {C : ℤ → Sort u_1} (nat : (n : ℕ) → C ↑n) (neg : ((n : ℕ) → C ↑n) → (n : ℕ) → C (-↑n)) (n : ℤ) : C n

Inductively define a function on ℤ by defining it on ℕ and extending it from n to -n.

Equations

• Int.negInduction nat neg (Int.ofNat n) = nat n
• Int.negInduction nat neg (Int.negSucc n) = neg nat (n + 1)

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

See Int.inductionOn' for an induction in both directions.

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

See Int.inductionOn' for an induction in both directions.

def Int.strongRec {m : ℤ} {P : ℤ → Sort u_1} (lt : (n : ℤ) → n < m → P n) (ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n) (n : ℤ) : P n

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.

Equations

• One or more equations did not get rendered due to their size.

theorem Int.strongRec_of_lt {m n : ℤ} {P : ℤ → Sort u_1} {lt : (n : ℤ) → n < m → P n} {ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n} (hn : n < m) : Int.strongRec lt ge n = lt n hn

theorem Int.strongRec_of_ge {m n : ℤ} {P : ℤ → Sort u_1} {lt : (n : ℤ) → n < m → P n} {ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n} (hn : m ≤ n) : Int.strongRec lt ge n = ge n hn fun (k : ℤ) (x : k < n) => Int.strongRec lt ge k

nat abs

@[simp]

theorem Int.natAbs_ofNat' (n : ℕ) : (ofNat n).natAbs = n

theorem Int.natAbs_add_of_nonneg {a b : ℤ} : 0 ≤ a → 0 ≤ b → (a + b).natAbs = a.natAbs + b.natAbs

theorem Int.natAbs_add_of_nonpos {a b : ℤ} (ha : a ≤ 0) (hb : b ≤ 0) : (a + b).natAbs = a.natAbs + b.natAbs

theorem Int.natAbs_surjective : Function.Surjective natAbs

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

theorem Int.pow_right_injective {a : ℤ} (h : 1 < a.natAbs) : Function.Injective fun (x : ℕ) => a ^ x

theorem Int.natAbs_sq (x : ℤ) : ↑x.natAbs ^ 2 = x ^ 2

theorem Int.natAbs_pow_two (x : ℤ) : ↑x.natAbs ^ 2 = x ^ 2

Alias of Int.natAbs_sq.

theorem Int.sign_mul_self_eq_natAbs (a : ℤ) : a.sign * a = ↑a.natAbs

/

@[simp]

theorem Int.natCast_div (m n : ℕ) : ↑(m / n) = ↑m / ↑n

theorem Int.natCast_ediv (m n : ℕ) : ↑(m / n) = (↑m).ediv ↑n

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

mod

@[simp]

theorem Int.natCast_mod (m n : ℕ) : ↑(m % n) = ↑m % ↑n

theorem Int.add_emod_eq_add_mod_right {m n k : ℤ} (i : ℤ) (H : m % n = k % n) : (m + i) % n = (k + i) % n

@[simp]

theorem Int.neg_emod_two (i : ℤ) : -i % 2 = i % 2

properties of / and %

theorem Int.emod_two_eq_zero_or_one (n : ℤ) : n % 2 = 0 ∨ n % 2 = 1

dvd

theorem Int.mul_dvd_mul {a b c d : ℤ} : a ∣ b → c ∣ d → a * c ∣ b * d

theorem Int.mul_dvd_mul_left {b c : ℤ} (a : ℤ) (h : b ∣ c) : a * b ∣ a * c

theorem Int.mul_dvd_mul_right {b c : ℤ} (a : ℤ) (h : b ∣ c) : b * a ∣ c * a

theorem Int.dvd_mul_of_div_dvd {a b c : ℤ} (h : b ∣ a) (hdiv : a / b ∣ c) : a ∣ b * c

@[simp]

theorem Int.div_dvd_iff_dvd_mul {a b c : ℤ} (h : b ∣ a) (hb : b ≠ 0) : a / b ∣ c ↔ a ∣ b * c

theorem Int.mul_dvd_of_dvd_div {a b c : ℤ} (hcb : c ∣ b) (h : a ∣ b / c) : c * a ∣ b

theorem Int.dvd_div_of_mul_dvd {a b c : ℤ} (h : a * b ∣ c) : b ∣ c / a

@[simp]

theorem Int.dvd_div_iff_mul_dvd {a b c : ℤ} (hbc : c ∣ b) : a ∣ b / c ↔ c * a ∣ b

theorem Int.ediv_dvd_ediv {a b c : ℤ} : a ∣ b → b ∣ c → b / a ∣ c / a

theorem Int.exists_lt_and_lt_iff_not_dvd {n : ℤ} (m : ℤ) (hn : 0 < n) : (∃ (k : ℤ), n * k < m ∧ m < n * (k + 1)) ↔ ¬n ∣ m

If n > 0 then m is not divisible by n iff it is between n * k and n * (k + 1) for some k.

theorem Int.natCast_dvd_natCast {m n : ℕ} : ↑m ∣ ↑n ↔ m ∣ n

theorem Int.natCast_dvd {n : ℤ} {m : ℕ} : ↑m ∣ n ↔ m ∣ n.natAbs

theorem Int.dvd_natCast {m : ℤ} {n : ℕ} : m ∣ ↑n ↔ m.natAbs ∣ n

theorem Int.natAbs_ediv (a b : ℤ) (H : b ∣ a) : (a / b).natAbs = a.natAbs / b.natAbs

theorem Int.dvd_of_mul_dvd_mul_left {a m n : ℤ} (ha : a ≠ 0) (h : a * m ∣ a * n) : m ∣ n

theorem Int.dvd_of_mul_dvd_mul_right {a m n : ℤ} (ha : a ≠ 0) (h : m * a ∣ n * a) : m ∣ n

theorem Int.eq_mul_div_of_mul_eq_mul_of_dvd_left {a b c d : ℤ} (hb : b ≠ 0) (hbc : b ∣ c) (h : b * a = c * d) : a = c / b * d

theorem Int.eq_zero_of_dvd_of_natAbs_lt_natAbs {m n : ℤ} (hmn : m ∣ n) (hnm : n.natAbs < m.natAbs) : n = 0

If an integer with larger absolute value divides an integer, it is zero.

theorem Int.eq_zero_of_dvd_of_nonneg_of_lt {m n : ℤ} (hm : 0 ≤ m) (hmn : m < n) (hnm : n ∣ m) : m = 0

theorem Int.eq_of_mod_eq_of_natAbs_sub_lt_natAbs {a b c : ℤ} (h1 : a % b = c) (h2 : (a - c).natAbs < b.natAbs) : a = c

If two integers are congruent to a sufficiently large modulus, they are equal.

theorem Int.ofNat_add_negSucc_of_ge {m n : ℕ} (h : n.succ ≤ m) : ofNat m + negSucc n = ofNat (m - n.succ)

theorem Int.natAbs_le_of_dvd_ne_zero {m n : ℤ} (hmn : m ∣ n) (hn : n ≠ 0) : m.natAbs ≤ n.natAbs

/ and ordering

theorem Int.natAbs_eq_of_dvd_dvd {m n : ℤ} (hmn : m ∣ n) (hnm : n ∣ m) : m.natAbs = n.natAbs

theorem Int.ediv_dvd_of_dvd {m n : ℤ} (hmn : m ∣ n) : n / m ∣ n

theorem Int.le_iff_pos_of_dvd {a b : ℤ} (ha : 0 < a) (hab : a ∣ b) : a ≤ b ↔ 0 < b

theorem Int.le_add_iff_lt_of_dvd_sub {a b c : ℤ} (ha : 0 < a) (hab : a ∣ c - b) : a + b ≤ c ↔ b < c

sign

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

theorem Int.sign_add_eq_of_sign_eq {m n : ℤ} : m.sign = n.sign → (m + n).sign = n.sign

toNat

@[simp]

theorem Int.toNat_natCast (n : ℕ) : (↑n).toNat = n

@[simp]

theorem Int.toNat_natCast_add_one {n : ℕ} : (↑n + 1).toNat = n + 1

@[simp]

theorem Int.toNat_le {m : ℤ} {n : ℕ} : m.toNat ≤ n ↔ m ≤ ↑n

@[simp]

theorem Int.lt_toNat {n : ℤ} {m : ℕ} : m < n.toNat ↔ ↑m < n

theorem Int.toNat_le_toNat {a b : ℤ} (h : a ≤ b) : a.toNat ≤ b.toNat

theorem Int.toNat_lt_toNat {a b : ℤ} (hb : 0 < b) : a.toNat < b.toNat ↔ a < b

theorem Int.lt_of_toNat_lt {a b : ℤ} (h : a.toNat < b.toNat) : a < b

@[simp]

theorem Int.toNat_pred_coe_of_pos {i : ℤ} (h : 0 < i) : ↑(i.toNat - 1) = i - 1

@[simp]

theorem Int.toNat_eq_zero {n : ℤ} : n.toNat = 0 ↔ n ≤ 0

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

theorem Int.toNat_lt' {m : ℤ} {n : ℕ} (hn : n ≠ 0) : m.toNat < n ↔ m < ↑n

def Int.natMod (m n : ℤ) : ℕ

The modulus of an integer by another as a natural. Uses the E-rounding convention.

Equations

• m.natMod n = (m % n).toNat

theorem Int.natMod_lt {m : ℤ} {n : ℕ} (hn : n ≠ 0) : m.natMod ↑n < n

@[simp]

theorem Int.pow_eq (m : ℤ) (n : ℕ) : m.pow n = m ^ n