Basic operations on the integers

This file contains some basic lemmas about integers.

See note [foundational algebra order theory].

This file should not depend on anything defined in Mathlib (except for notation), so that it can be upstreamed to Batteries easily.

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

succ and pred

def Int.succ (a : ℤ) : ℤ

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

def Int.pred (a : ℤ) : ℤ

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

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.induction_on {motive : ℤ → Prop} (i : ℤ) (zero : motive 0) (succ : ∀ (i : ℕ), motive ↑i → motive (↑i + 1)) (pred : ∀ (i : ℕ), motive (-↑i) → motive (-↑i - 1)) : motive i

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.

def Int.inductionOn' {motive : ℤ → Sort u_1} (z b : ℤ) (zero : motive b) (succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)) (pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)) : motive 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.

def Int.inductionOn'.pos {motive : ℤ → Sort u_1} (b : ℤ) (zero : motive b) (succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)) (n : ℕ) : motive (b + ↑n)

The positive case of Int.inductionOn'.

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

The negative case of Int.inductionOn'.

theorem Int.inductionOn'_self {motive : ℤ → Sort u_1} {b : ℤ} {zero : motive b} {succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)} {pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)} : Int.inductionOn' b b zero succ pred = zero

theorem Int.inductionOn'_sub_one {motive : ℤ → Sort u_1} {z b : ℤ} {zero : motive b} {succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)} {pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)} (hz : z ≤ b) : Int.inductionOn' (z - 1) b zero succ pred = pred z hz (Int.inductionOn' z b zero succ pred)

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

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

theorem Int.le_induction {m : ℤ} {motive : (n : ℤ) → m ≤ n → Prop} (base : motive m ⋯) (succ : ∀ (n : ℤ) (hmn : m ≤ n), motive n hmn → motive (n + 1) ⋯) (n : ℤ) (hmn : m ≤ n) : motive n hmn

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

theorem Int.le_induction_down {m : ℤ} {motive : (n : ℤ) → n ≤ m → Prop} (base : motive m ⋯) (pred : ∀ (n : ℤ) (hmn : n ≤ m), motive n hmn → motive (n - 1) ⋯) (n : ℤ) (hmn : n ≤ m) : motive n hmn

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

def Int.strongRec {m : ℤ} {motive : ℤ → Sort u_1} (lt : (n : ℤ) → n < m → motive n) (ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → motive k) → motive n) (n : ℤ) : motive 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.

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

mul

natAbs

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

Alias of Int.natAbs_pow_two.

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

/

theorem Int.natCast_div (m n : ℕ) : ↑(m / n) = ↑m / ↑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.div_le_iff_of_dvd_of_pos {a b c : ℤ} (hb : 0 < b) (hba : b ∣ a) : a / b ≤ c ↔ a ≤ b * c

theorem Int.div_le_iff_of_dvd_of_neg {a b c : ℤ} (hb : b < 0) (hba : b ∣ a) : a / b ≤ c ↔ b * c ≤ a

theorem Int.div_lt_iff_of_dvd_of_pos {a b c : ℤ} (hb : 0 < b) (hba : b ∣ a) : a / b < c ↔ a < b * c

theorem Int.div_lt_iff_of_dvd_of_neg {a b c : ℤ} (hb : b < 0) (hba : b ∣ a) : a / b < c ↔ b * c < a

theorem Int.le_div_iff_of_dvd_of_pos {a b c : ℤ} (hc : 0 < c) (hcb : c ∣ b) : a ≤ b / c ↔ c * a ≤ b

theorem Int.le_div_iff_of_dvd_of_neg {a b c : ℤ} (hc : c < 0) (hcb : c ∣ b) : a ≤ b / c ↔ b ≤ c * a

theorem Int.lt_div_iff_of_dvd_of_pos {a b c : ℤ} (hc : 0 < c) (hcb : c ∣ b) : a < b / c ↔ c * a < b

theorem Int.lt_div_iff_of_dvd_of_neg {a b c : ℤ} (hc : c < 0) (hcb : c ∣ b) : a < b / c ↔ b < c * a

theorem Int.div_le_div_iff_of_dvd_of_pos_of_pos {a b c d : ℤ} (hb : 0 < b) (hd : 0 < d) (hba : b ∣ a) (hdc : d ∣ c) : a / b ≤ c / d ↔ d * a ≤ c * b

theorem Int.div_le_div_iff_of_dvd_of_pos_of_neg {a b c d : ℤ} (hb : 0 < b) (hd : d < 0) (hba : b ∣ a) (hdc : d ∣ c) : a / b ≤ c / d ↔ c * b ≤ d * a

theorem Int.div_le_div_iff_of_dvd_of_neg_of_pos {a b c d : ℤ} (hb : b < 0) (hd : 0 < d) (hba : b ∣ a) (hdc : d ∣ c) : a / b ≤ c / d ↔ c * b ≤ d * a

theorem Int.div_le_div_iff_of_dvd_of_neg_of_neg {a b c d : ℤ} (hb : b < 0) (hd : d < 0) (hba : b ∣ a) (hdc : d ∣ c) : a / b ≤ c / d ↔ d * a ≤ c * b

theorem Int.div_lt_div_iff_of_dvd_of_pos {a b c d : ℤ} (hb : 0 < b) (hd : 0 < d) (hba : b ∣ a) (hdc : d ∣ c) : a / b < c / d ↔ d * a < c * b

theorem Int.div_lt_div_iff_of_dvd_of_pos_of_neg {a b c d : ℤ} (hb : 0 < b) (hd : d < 0) (hba : b ∣ a) (hdc : d ∣ c) : a / b < c / d ↔ c * b < d * a

theorem Int.div_lt_div_iff_of_dvd_of_neg_of_pos {a b c d : ℤ} (hb : b < 0) (hd : 0 < d) (hba : b ∣ a) (hdc : d ∣ c) : a / b < c / d ↔ c * b < d * a

theorem Int.div_lt_div_iff_of_dvd_of_neg_of_neg {a b c d : ℤ} (hb : b < 0) (hd : d < 0) (hba : b ∣ a) (hdc : d ∣ c) : a / b < c / d ↔ d * a < c * b

properties of / and %

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

dvd

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

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

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

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.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.ofNat_add_negSucc_of_ge {m n : ℕ} (h : n.succ ≤ m) : ofNat m + negSucc n = ofNat (m - n.succ)

/ and ordering

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_add_eq_of_sign_eq {m n : ℤ} : m.sign = n.sign → (m + n).sign = n.sign

toNat

@[simp]

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

theorem Int.toNat_lt_of_ne_zero {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.

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

For use in Mathlib/Tactic/NormNum/Pow.lean

@[simp]

theorem Int.gcd_ofNat_negSucc (m n : ℕ) : (↑m).gcd (negSucc n) = m.gcd (n + 1)

@[simp]

theorem Int.gcd_negSucc_ofNat (m n : ℕ) : (negSucc m).gcd ↑n = (m + 1).gcd n

@[simp]

theorem Int.gcd_negSucc_negSucc (m n : ℕ) : (negSucc m).gcd (negSucc n) = (m + 1).gcd (n + 1)