Mathlib.Data.Int.Order.Basic

Int.le.elim theorem

{a b : ℤ} (h : a ≤ b) {P : Prop} (h' : ∀ n : ℕ, a + ↑n = b → P) : P

Full source

theorem le.elim {a b : ℤ} (h : a ≤ b) {P : Prop} (h' : ∀ n : ℕ, a + ↑n = b → P) : P :=
  Exists.elim (le.dest h) h'

Elimination Rule for Integer Inequality $a \leq b$ via Natural Number Shift

Informal description

For any integers $a$ and $b$ such that $a \leq b$, and for any proposition $P$, if for every natural number $n$ the equality $a + n = b$ implies $P$, then $P$ holds.

Int.lt.elim theorem

{a b : ℤ} (h : a < b) {P : Prop} (h' : ∀ n : ℕ, a + ↑(Nat.succ n) = b → P) : P

Full source

theorem lt.elim {a b : ℤ} (h : a < b) {P : Prop} (h' : ∀ n : ℕ, a + ↑(Nat.succ n) = b → P) : P :=
  Exists.elim (lt.dest h) h'

Elimination Rule for Integer Less-Than Relation

Informal description

For any integers $a$ and $b$ such that $a < b$, and for any proposition $P$, if for every natural number $n$ the equality $a + (n + 1) = b$ implies $P$, then $P$ holds.

Int.instLinearOrder instance

: LinearOrder ℤ

Full source

instance instLinearOrder : LinearOrder ℤ where
  le := (·≤·)
  le_refl := Int.le_refl
  le_trans := @Int.le_trans
  le_antisymm := @Int.le_antisymm
  lt := (·<·)
  lt_iff_le_not_le := @Int.lt_iff_le_not_le
  le_total := Int.le_total
  toDecidableEq := by infer_instance
  toDecidableLE := by infer_instance
  toDecidableLT := by infer_instance

The Linear Order Structure on Integers

Informal description

The integers $\mathbb{Z}$ are equipped with a canonical linear order structure, where the relation $\leq$ is reflexive, transitive, antisymmetric, and total.

Int.nonneg_or_nonpos_of_mul_nonneg theorem

{a b : ℤ} : 0 ≤ a * b → 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Full source

theorem nonneg_or_nonpos_of_mul_nonneg {a b : ℤ} : 0 ≤ a * b → 0 ≤ a ∧ 0 ≤ b0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 := by
  intro h
  by_cases ha : 0 ≤ a <;> by_cases hb : 0 ≤ b
  · exact .inl ⟨ha, hb⟩
  · refine .inr ⟨?_, le_of_not_le hb⟩
    obtain _ | _ := Int.mul_eq_zero.mp <|
      Int.le_antisymm (Int.mul_nonpos_of_nonneg_of_nonpos ha <| le_of_not_le hb) h
    all_goals omega
  · refine .inr ⟨le_of_not_le ha, ?_⟩
    obtain _ | _ := Int.mul_eq_zero.mp <|
      Int.le_antisymm (Int.mul_nonpos_of_nonpos_of_nonneg (le_of_not_le ha) hb) h
    all_goals omega
  · exact .inr ⟨le_of_not_ge ha, le_of_not_ge hb⟩

Non-Negative Product Implies Non-Negative or Non-Positive Factors in Integers

Informal description

For any integers $a$ and $b$, if the product $a \cdot b$ is non-negative (i.e., $0 \leq a \cdot b$), then either both $a$ and $b$ are non-negative (i.e., $0 \leq a$ and $0 \leq b$) or both are non-positive (i.e., $a \leq 0$ and $b \leq 0$).

Int.mul_nonneg_of_nonneg_or_nonpos theorem

{a b : ℤ} : 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 → 0 ≤ a * b

Full source

theorem mul_nonneg_of_nonneg_or_nonpos {a b : ℤ} : 0 ≤ a ∧ 0 ≤ b0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 → 0 ≤ a * b
  | .inl ⟨ha, hb⟩ => Int.mul_nonneg ha hb
  | .inr ⟨ha, hb⟩ => Int.mul_nonneg_of_nonpos_of_nonpos ha hb

Product of Non-Negative or Non-Positive Integers is Non-Negative

Informal description

For any integers $a$ and $b$, if either both $a$ and $b$ are non-negative or both are non-positive, then their product $a \cdot b$ is non-negative.

Int.mul_nonneg_iff theorem

{a b : ℤ} : 0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Full source

protected theorem mul_nonneg_iff {a b : ℤ} : 0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 :=
  ⟨nonneg_or_nonpos_of_mul_nonneg, mul_nonneg_of_nonneg_or_nonpos⟩

Characterization of Non-Negative Integer Products: $0 \leq a \cdot b \leftrightarrow (0 \leq a \land 0 \leq b) \lor (a \leq 0 \land b \leq 0)$

Informal description

For any integers $a$ and $b$, the product $a \cdot b$ is non-negative (i.e., $0 \leq a \cdot b$) if and only if either both $a$ and $b$ are non-negative (i.e., $0 \leq a$ and $0 \leq b$) or both are non-positive (i.e., $a \leq 0$ and $b \leq 0$).