lt_four — Mathlib

English

If q ≤ r and 1 < sumInv {2,q,r}, then q < 4.

Русский

Если q ≤ r и 1 < sumInv {2,q,r}, то q < 4.

LaTeX

$$$\forall q,r \in \mathbb{N}_{+},\ q \le r \Rightarrow 1 < \operatorname{sumInv}\{2,q,r\} \Rightarrow q < 4$$$

Lean4

theorem lt_four {q r : ℕ+} (hqr : q ≤ r) (H : 1 < sumInv { 2, q, r }) : q < 4 :=
  by
  have h4 : (0 : ℚ) < 4 := by simp
  contrapose! H
  rw [sumInv_pqr]
  have h4r := H.trans hqr
  have hq : (q : ℚ)⁻¹ ≤ 4⁻¹ := by
    rw [inv_le_inv₀ _ h4]
    · assumption_mod_cast
    · simp
  have hr : (r : ℚ)⁻¹ ≤ 4⁻¹ := by
    rw [inv_le_inv₀ _ h4]
    · assumption_mod_cast
    · simp
  calc
    (2⁻¹ + (q : ℚ)⁻¹ + (r : ℚ)⁻¹) ≤ 2⁻¹ + 4⁻¹ + 4⁻¹ := add_le_add (add_le_add le_rfl hq) hr
    _ = 1 := by norm_num

Похожие утверждения