Results about the order properties of the integers, and the integers as an ordered ring.

Order properties of the integers

theorem Int.lt_of_not_ge {a : Int} {b : Int} : ¬a ≤ b → b < a

Alias of the forward direction of Int.not_le.

theorem Int.not_le_of_gt {a : Int} {b : Int} : b < a → ¬a ≤ b

Alias of the reverse direction of Int.not_le.

theorem Int.le_of_not_le {a : Int} {b : Int} : ¬a ≤ b → b ≤ a

@[simp]

theorem Int.negSucc_not_pos (n : Nat) : 0 < Int.negSucc n ↔ False

theorem Int.eq_negSucc_of_lt_zero {a : Int} : a < 0 → ∃ (n : Nat), a = Int.negSucc n

theorem Int.lt_of_add_lt_add_left {a : Int} {b : Int} {c : Int} (h : a + b < a + c) : b < c

theorem Int.lt_of_add_lt_add_right {a : Int} {b : Int} {c : Int} (h : a + b < c + b) : a < c

theorem Int.add_lt_add_iff_left {b : Int} {c : Int} (a : Int) : a + b < a + c ↔ b < c

theorem Int.add_lt_add_iff_right {a : Int} {b : Int} (c : Int) : a + c < b + c ↔ a < b

theorem Int.add_lt_add {a : Int} {b : Int} {c : Int} {d : Int} (h₁ : a < b) (h₂ : c < d) : a + c < b + d

theorem Int.add_lt_add_of_le_of_lt {a : Int} {b : Int} {c : Int} {d : Int} (h₁ : a ≤ b) (h₂ : c < d) : a + c < b + d

theorem Int.add_lt_add_of_lt_of_le {a : Int} {b : Int} {c : Int} {d : Int} (h₁ : a < b) (h₂ : c ≤ d) : a + c < b + d

theorem Int.lt_add_of_pos_right (a : Int) {b : Int} (h : 0 < b) : a < a + b

theorem Int.lt_add_of_pos_left (a : Int) {b : Int} (h : 0 < b) : a < b + a

theorem Int.add_nonneg {a : Int} {b : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a + b

theorem Int.add_pos {a : Int} {b : Int} (ha : 0 < a) (hb : 0 < b) : 0 < a + b

theorem Int.add_pos_of_pos_of_nonneg {a : Int} {b : Int} (ha : 0 < a) (hb : 0 ≤ b) : 0 < a + b

theorem Int.add_pos_of_nonneg_of_pos {a : Int} {b : Int} (ha : 0 ≤ a) (hb : 0 < b) : 0 < a + b

theorem Int.add_nonpos {a : Int} {b : Int} (ha : a ≤ 0) (hb : b ≤ 0) : a + b ≤ 0

theorem Int.add_neg {a : Int} {b : Int} (ha : a < 0) (hb : b < 0) : a + b < 0

theorem Int.add_neg_of_neg_of_nonpos {a : Int} {b : Int} (ha : a < 0) (hb : b ≤ 0) : a + b < 0

theorem Int.add_neg_of_nonpos_of_neg {a : Int} {b : Int} (ha : a ≤ 0) (hb : b < 0) : a + b < 0

theorem Int.lt_add_of_le_of_pos {a : Int} {b : Int} {c : Int} (hbc : b ≤ c) (ha : 0 < a) : b < c + a

theorem Int.add_one_le_iff {a : Int} {b : Int} : a + 1 ≤ b ↔ a < b

theorem Int.lt_add_one_iff {a : Int} {b : Int} : a < b + 1 ↔ a ≤ b

@[simp]

theorem Int.succ_ofNat_pos (n : Nat) : 0 < ↑n + 1

theorem Int.le_add_one {a : Int} {b : Int} (h : a ≤ b) : a ≤ b + 1

theorem Int.nonneg_of_neg_nonpos {a : Int} (h : -a ≤ 0) : 0 ≤ a

theorem Int.nonpos_of_neg_nonneg {a : Int} (h : 0 ≤ -a) : a ≤ 0

theorem Int.lt_of_neg_lt_neg {a : Int} {b : Int} (h : -b < -a) : a < b

theorem Int.pos_of_neg_neg {a : Int} (h : -a < 0) : 0 < a

theorem Int.neg_of_neg_pos {a : Int} (h : 0 < -a) : a < 0

theorem Int.le_neg_of_le_neg {a : Int} {b : Int} (h : a ≤ -b) : b ≤ -a

theorem Int.neg_le_of_neg_le {a : Int} {b : Int} (h : -a ≤ b) : -b ≤ a

theorem Int.lt_neg_of_lt_neg {a : Int} {b : Int} (h : a < -b) : b < -a

theorem Int.neg_lt_of_neg_lt {a : Int} {b : Int} (h : -a < b) : -b < a

theorem Int.sub_nonpos_of_le {a : Int} {b : Int} (h : a ≤ b) : a - b ≤ 0

theorem Int.le_of_sub_nonpos {a : Int} {b : Int} (h : a - b ≤ 0) : a ≤ b

theorem Int.sub_neg_of_lt {a : Int} {b : Int} (h : a < b) : a - b < 0

theorem Int.lt_of_sub_neg {a : Int} {b : Int} (h : a - b < 0) : a < b

theorem Int.add_le_of_le_neg_add {a : Int} {b : Int} {c : Int} (h : b ≤ -a + c) : a + b ≤ c

theorem Int.le_neg_add_of_add_le {a : Int} {b : Int} {c : Int} (h : a + b ≤ c) : b ≤ -a + c

theorem Int.add_le_of_le_sub_left {a : Int} {b : Int} {c : Int} (h : b ≤ c - a) : a + b ≤ c

theorem Int.le_sub_left_of_add_le {a : Int} {b : Int} {c : Int} (h : a + b ≤ c) : b ≤ c - a

theorem Int.add_le_of_le_sub_right {a : Int} {b : Int} {c : Int} (h : a ≤ c - b) : a + b ≤ c

theorem Int.le_sub_right_of_add_le {a : Int} {b : Int} {c : Int} (h : a + b ≤ c) : a ≤ c - b

theorem Int.le_add_of_neg_add_le {a : Int} {b : Int} {c : Int} (h : -b + a ≤ c) : a ≤ b + c

theorem Int.neg_add_le_of_le_add {a : Int} {b : Int} {c : Int} (h : a ≤ b + c) : -b + a ≤ c

theorem Int.le_add_of_sub_left_le {a : Int} {b : Int} {c : Int} (h : a - b ≤ c) : a ≤ b + c

theorem Int.le_add_of_sub_right_le {a : Int} {b : Int} {c : Int} (h : a - c ≤ b) : a ≤ b + c

theorem Int.sub_right_le_of_le_add {a : Int} {b : Int} {c : Int} (h : a ≤ b + c) : a - c ≤ b

theorem Int.le_add_of_neg_add_le_left {a : Int} {b : Int} {c : Int} (h : -b + a ≤ c) : a ≤ b + c

theorem Int.neg_add_le_left_of_le_add {a : Int} {b : Int} {c : Int} (h : a ≤ b + c) : -b + a ≤ c

theorem Int.le_add_of_neg_add_le_right {a : Int} {b : Int} {c : Int} (h : -c + a ≤ b) : a ≤ b + c

theorem Int.neg_add_le_right_of_le_add {a : Int} {b : Int} {c : Int} (h : a ≤ b + c) : -c + a ≤ b

theorem Int.le_add_of_neg_le_sub_left {a : Int} {b : Int} {c : Int} (h : -a ≤ b - c) : c ≤ a + b

theorem Int.neg_le_sub_left_of_le_add {a : Int} {b : Int} {c : Int} (h : c ≤ a + b) : -a ≤ b - c

theorem Int.le_add_of_neg_le_sub_right {a : Int} {b : Int} {c : Int} (h : -b ≤ a - c) : c ≤ a + b

theorem Int.neg_le_sub_right_of_le_add {a : Int} {b : Int} {c : Int} (h : c ≤ a + b) : -b ≤ a - c

theorem Int.sub_le_of_sub_le {a : Int} {b : Int} {c : Int} (h : a - b ≤ c) : a - c ≤ b

theorem Int.sub_le_sub_left {a : Int} {b : Int} (h : a ≤ b) (c : Int) : c - b ≤ c - a

theorem Int.sub_le_sub_right {a : Int} {b : Int} (h : a ≤ b) (c : Int) : a - c ≤ b - c

theorem Int.sub_le_sub {a : Int} {b : Int} {c : Int} {d : Int} (hab : a ≤ b) (hcd : c ≤ d) : a - d ≤ b - c

theorem Int.add_lt_of_lt_neg_add {a : Int} {b : Int} {c : Int} (h : b < -a + c) : a + b < c

theorem Int.lt_neg_add_of_add_lt {a : Int} {b : Int} {c : Int} (h : a + b < c) : b < -a + c

theorem Int.add_lt_of_lt_sub_left {a : Int} {b : Int} {c : Int} (h : b < c - a) : a + b < c

theorem Int.lt_sub_left_of_add_lt {a : Int} {b : Int} {c : Int} (h : a + b < c) : b < c - a

theorem Int.add_lt_of_lt_sub_right {a : Int} {b : Int} {c : Int} (h : a < c - b) : a + b < c

theorem Int.lt_sub_right_of_add_lt {a : Int} {b : Int} {c : Int} (h : a + b < c) : a < c - b

theorem Int.lt_add_of_neg_add_lt {a : Int} {b : Int} {c : Int} (h : -b + a < c) : a < b + c

theorem Int.neg_add_lt_of_lt_add {a : Int} {b : Int} {c : Int} (h : a < b + c) : -b + a < c

theorem Int.lt_add_of_sub_left_lt {a : Int} {b : Int} {c : Int} (h : a - b < c) : a < b + c

theorem Int.sub_left_lt_of_lt_add {a : Int} {b : Int} {c : Int} (h : a < b + c) : a - b < c

theorem Int.lt_add_of_sub_right_lt {a : Int} {b : Int} {c : Int} (h : a - c < b) : a < b + c

theorem Int.sub_right_lt_of_lt_add {a : Int} {b : Int} {c : Int} (h : a < b + c) : a - c < b

theorem Int.lt_add_of_neg_add_lt_left {a : Int} {b : Int} {c : Int} (h : -b + a < c) : a < b + c

theorem Int.neg_add_lt_left_of_lt_add {a : Int} {b : Int} {c : Int} (h : a < b + c) : -b + a < c

theorem Int.lt_add_of_neg_add_lt_right {a : Int} {b : Int} {c : Int} (h : -c + a < b) : a < b + c

theorem Int.neg_add_lt_right_of_lt_add {a : Int} {b : Int} {c : Int} (h : a < b + c) : -c + a < b

theorem Int.lt_add_of_neg_lt_sub_left {a : Int} {b : Int} {c : Int} (h : -a < b - c) : c < a + b

theorem Int.neg_lt_sub_left_of_lt_add {a : Int} {b : Int} {c : Int} (h : c < a + b) : -a < b - c

theorem Int.lt_add_of_neg_lt_sub_right {a : Int} {b : Int} {c : Int} (h : -b < a - c) : c < a + b

theorem Int.neg_lt_sub_right_of_lt_add {a : Int} {b : Int} {c : Int} (h : c < a + b) : -b < a - c

theorem Int.sub_lt_of_sub_lt {a : Int} {b : Int} {c : Int} (h : a - b < c) : a - c < b

theorem Int.sub_lt_sub_left {a : Int} {b : Int} (h : a < b) (c : Int) : c - b < c - a

theorem Int.sub_lt_sub_right {a : Int} {b : Int} (h : a < b) (c : Int) : a - c < b - c

theorem Int.sub_lt_sub {a : Int} {b : Int} {c : Int} {d : Int} (hab : a < b) (hcd : c < d) : a - d < b - c

theorem Int.sub_lt_sub_of_le_of_lt {a : Int} {b : Int} {c : Int} {d : Int} (hab : a ≤ b) (hcd : c < d) : a - d < b - c

theorem Int.sub_lt_sub_of_lt_of_le {a : Int} {b : Int} {c : Int} {d : Int} (hab : a < b) (hcd : c ≤ d) : a - d < b - c

theorem Int.add_le_add_three {a : Int} {b : Int} {c : Int} {d : Int} {e : Int} {f : Int} (h₁ : a ≤ d) (h₂ : b ≤ e) (h₃ : c ≤ f) : a + b + c ≤ d + e + f

theorem Int.exists_eq_neg_ofNat {a : Int} (H : a ≤ 0) : ∃ (n : Nat), a = -↑n

theorem Int.lt_of_add_one_le {a : Int} {b : Int} (H : a + 1 ≤ b) : a < b

theorem Int.lt_add_one_of_le {a : Int} {b : Int} (H : a ≤ b) : a < b + 1

theorem Int.le_of_lt_add_one {a : Int} {b : Int} (H : a < b + 1) : a ≤ b

theorem Int.sub_one_lt_of_le {a : Int} {b : Int} (H : a ≤ b) : a - 1 < b

theorem Int.le_of_sub_one_lt {a : Int} {b : Int} (H : a - 1 < b) : a ≤ b

theorem Int.le_sub_one_of_lt {a : Int} {b : Int} (H : a < b) : a ≤ b - 1

theorem Int.lt_of_le_sub_one {a : Int} {b : Int} (H : a ≤ b - 1) : a < b

theorem Int.mul_lt_mul {a : Int} {b : Int} {c : Int} {d : Int} (h₁ : a < c) (h₂ : b ≤ d) (h₃ : 0 < b) (h₄ : 0 ≤ c) : a * b < c * d

theorem Int.mul_lt_mul' {a : Int} {b : Int} {c : Int} {d : Int} (h₁ : a ≤ c) (h₂ : b < d) (h₃ : 0 ≤ b) (h₄ : 0 < c) : a * b < c * d

theorem Int.mul_neg_of_pos_of_neg {a : Int} {b : Int} (ha : 0 < a) (hb : b < 0) : a * b < 0

theorem Int.mul_neg_of_neg_of_pos {a : Int} {b : Int} (ha : a < 0) (hb : 0 < b) : a * b < 0

theorem Int.mul_nonneg_of_nonpos_of_nonpos {a : Int} {b : Int} (ha : a ≤ 0) (hb : b ≤ 0) : 0 ≤ a * b

theorem Int.mul_lt_mul_of_neg_left {a : Int} {b : Int} {c : Int} (h : b < a) (hc : c < 0) : c * a < c * b

theorem Int.mul_lt_mul_of_neg_right {a : Int} {b : Int} {c : Int} (h : b < a) (hc : c < 0) : a * c < b * c

theorem Int.mul_pos_of_neg_of_neg {a : Int} {b : Int} (ha : a < 0) (hb : b < 0) : 0 < a * b

theorem Int.mul_self_le_mul_self {a : Int} {b : Int} (h1 : 0 ≤ a) (h2 : a ≤ b) : a * a ≤ b * b

theorem Int.mul_self_lt_mul_self {a : Int} {b : Int} (h1 : 0 ≤ a) (h2 : a < b) : a * a < b * b

@[simp]

theorem Int.sign_zero : Int.sign 0 = 0

@[simp]

theorem Int.sign_one : Int.sign 1 = 1

theorem Int.sign_neg_one : Int.sign (-1) = -1

@[simp]

theorem Int.sign_of_add_one (x : Nat) : Int.sign (↑x + 1) = 1

@[simp]

theorem Int.sign_negSucc (x : Nat) : Int.sign (Int.negSucc x) = -1

theorem Int.natAbs_sign (z : Int) : Int.natAbs (Int.sign z) = if z = 0 then 0 else 1

theorem Int.natAbs_sign_of_nonzero {z : Int} (hz : z ≠ 0) : Int.natAbs (Int.sign z) = 1

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

@[simp]

theorem Int.sign_neg (z : Int) : Int.sign (-z) = -Int.sign z

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

@[simp]

theorem Int.sign_mul (a : Int) (b : Int) : Int.sign (a * b) = Int.sign a * Int.sign b

theorem Int.sign_eq_one_of_pos {a : Int} (h : 0 < a) : Int.sign a = 1

theorem Int.sign_eq_neg_one_of_neg {a : Int} (h : a < 0) : Int.sign a = -1

theorem Int.eq_zero_of_sign_eq_zero {a : Int} : Int.sign a = 0 → a = 0

theorem Int.pos_of_sign_eq_one {a : Int} : Int.sign a = 1 → 0 < a

theorem Int.neg_of_sign_eq_neg_one {a : Int} : Int.sign a = -1 → a < 0

theorem Int.sign_eq_one_iff_pos (a : Int) : Int.sign a = 1 ↔ 0 < a

theorem Int.sign_eq_neg_one_iff_neg (a : Int) : Int.sign a = -1 ↔ a < 0

@[simp]

theorem Int.sign_eq_zero_iff_zero (a : Int) : Int.sign a = 0 ↔ a = 0

@[simp]

theorem Int.sign_sign {x : Int} : Int.sign (Int.sign x) = Int.sign x

@[simp]

theorem Int.sign_nonneg {x : Int} : 0 ≤ Int.sign x ↔ 0 ≤ x

theorem Int.natAbs_ne_zero {a : Int} : Int.natAbs a ≠ 0 ↔ a ≠ 0

theorem Int.natAbs_mul_self {a : Int} : ↑(Int.natAbs a * Int.natAbs a) = a * a

theorem Int.eq_nat_or_neg (a : Int) : ∃ (n : Nat), a = ↑n ∨ a = -↑n

theorem Int.natAbs_mul_natAbs_eq {a : Int} {b : Int} {c : Nat} (h : a * b = ↑c) : Int.natAbs a * Int.natAbs b = c

@[simp]

theorem Int.natAbs_mul_self' (a : Int) : ↑(Int.natAbs a) * ↑(Int.natAbs a) = a * a

theorem Int.natAbs_eq_iff {a : Int} {n : Nat} : Int.natAbs a = n ↔ a = ↑n ∨ a = -↑n

@[deprecated Int.natAbs_of_nonneg]

theorem Int.ofNat_natAbs_eq_of_nonneg {a : Int} (H : 0 ≤ a) : ↑(Int.natAbs a) = a

Alias of Int.natAbs_of_nonneg.

theorem Int.natAbs_add_le (a : Int) (b : Int) : Int.natAbs (a + b) ≤ Int.natAbs a + Int.natAbs b

theorem Int.natAbs_sub_le (a : Int) (b : Int) : Int.natAbs (a - b) ≤ Int.natAbs a + Int.natAbs b

theorem Int.negSucc_eq' (m : Nat) : Int.negSucc m = -↑m - 1

theorem Int.natAbs_lt_natAbs_of_nonneg_of_lt {a : Int} {b : Int} (w₁ : 0 ≤ a) (w₂ : a < b) : Int.natAbs a < Int.natAbs b

theorem Int.eq_natAbs_iff_mul_eq_zero {a : Int} {n : Nat} : Int.natAbs a = n ↔ (a - ↑n) * (a + ↑n) = 0

toNat

theorem Int.mem_toNat' (a : Int) (n : Nat) : Int.toNat' a = some n ↔ a = ↑n