English
If p ≤ q ≤ r and 1 < sumInv {p,q,r}, then p < 3.
Русский
Если p ≤ q ≤ r и 1 < sumInv {p,q,r}, то p < 3.
LaTeX
$$$\forall p,q,r \in \mathbb{N}_{+},\ p \le q \le r \wedge 1 < \operatorname{sumInv}\{p,q,r\} \Rightarrow p < 3$$$
Lean4
theorem lt_three {p q r : ℕ+} (hpq : p ≤ q) (hqr : q ≤ r) (H : 1 < sumInv { p, q, r }) : p < 3 :=
by
have h3 : (0 : ℚ) < 3 := by simp
contrapose! H
rw [sumInv_pqr]
have h3q := H.trans hpq
have h3r := h3q.trans hqr
have hp : (p : ℚ)⁻¹ ≤ 3⁻¹ := by
rw [inv_le_inv₀ _ h3]
· assumption_mod_cast
· simp
have hq : (q : ℚ)⁻¹ ≤ 3⁻¹ := by
rw [inv_le_inv₀ _ h3]
· assumption_mod_cast
· simp
have hr : (r : ℚ)⁻¹ ≤ 3⁻¹ := by
rw [inv_le_inv₀ _ h3]
· assumption_mod_cast
· simp
calc
(p : ℚ)⁻¹ + (q : ℚ)⁻¹ + (r : ℚ)⁻¹ ≤ 3⁻¹ + 3⁻¹ + 3⁻¹ := add_le_add (add_le_add hp hq) hr
_ = 1 := by norm_num
