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