lt_six — Mathlib

English

If 1 < sumInv {2,3,r}, then r < 6.

Русский

Если 1 < sumInv {2,3,r}, то r < 6.

LaTeX

$$$1 < \operatorname{sumInv}\{2,3,r\} \Rightarrow r < 6$$$

Lean4

theorem lt_six {r : ℕ+} (H : 1 < sumInv { 2, 3, r }) : r < 6 :=
  by
  have h6 : (0 : ℚ) < 6 := by simp
  contrapose! H
  rw [sumInv_pqr]
  have hr : (r : ℚ)⁻¹ ≤ 6⁻¹ := by
    rw [inv_le_inv₀ _ h6]
    · assumption_mod_cast
    · simp
  calc
    (2⁻¹ + 3⁻¹ + (r : ℚ)⁻¹ : ℚ) ≤ 2⁻¹ + 3⁻¹ + 6⁻¹ := add_le_add (add_le_add le_rfl le_rfl) hr
    _ = 1 := by norm_num

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