q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
h4 : 0 < 4
⊢ q < 4
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
⊢ q < 4
have h4 : (0 : ℚ) < 4 := by norm_num
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : ¬q < 4
⊢ sumInv {2, q, r} ≤ 1
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
h4 : 0 < 4
⊢ q < 4
contrapose! H
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : ¬q < 4
⊢ (↑↑2)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : ¬q < 4
⊢ sumInv {2, q, r} ≤ 1
rw [sumInv_pqr]
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : ¬q < 4
h4r : 4 ≤ r
⊢ (↑↑2)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : ¬q < 4
⊢ (↑↑2)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
have h4r := (not_lt.mp H).trans hqr
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
h4r : 4 ≤ r
H : 4 ≤ q
⊢ (↑↑2)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : ¬q < 4
h4r : 4 ≤ r
⊢ (↑↑2)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
simp at H
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
h4r : 4 ≤ r
H : 4 ≤ q
hq : (↑↑q)⁻¹ ≤ 4⁻¹
⊢ (↑↑2)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
h4r : 4 ≤ r
H : 4 ≤ q
⊢ (↑↑2)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
have hq: (q : ℚ)⁻¹ ≤ 4⁻¹ := by
  rw [inv_le_inv _ h4]
  assumption_mod_cast
  norm_num
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
h4r : 4 ≤ r
H : 4 ≤ q
hq : (↑↑q)⁻¹ ≤ 4⁻¹
hr : (↑↑r)⁻¹ ≤ 4⁻¹
⊢ (↑↑2)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
h4r : 4 ≤ r
H : 4 ≤ q
hq : (↑↑q)⁻¹ ≤ 4⁻¹
⊢ (↑↑2)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
have hr: (r : ℚ)⁻¹ ≤ 4⁻¹ := by
  rw [inv_le_inv _ h4]
  assumption_mod_cast
  norm_num
no goals
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
h4r : 4 ≤ r
H : 4 ≤ q
hq : (↑↑q)⁻¹ ≤ 4⁻¹
hr : (↑↑r)⁻¹ ≤ 4⁻¹
⊢ (↑↑2)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
calc
  (2⁻¹ + (q : ℚ)⁻¹ + (r : ℚ)⁻¹) ≤ 2⁻¹ + 4⁻¹ + 4⁻¹ := add_le_add (add_le_add le_rfl hq) hr
  _ = 1 := by norm_num
no goals
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
⊢ 0 < 4
norm_num
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
h4r : 4 ≤ r
H : 4 ≤ q
⊢ 4 ≤ ↑↑q

q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
h4r : 4 ≤ r
H : 4 ≤ q
⊢ 0 < ↑↑q
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
h4r : 4 ≤ r
H : 4 ≤ q
⊢ (↑↑q)⁻¹ ≤ 4⁻¹
rw [inv_le_inv _ h4]
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
h4r : 4 ≤ r
H : 4 ≤ q
⊢ 0 < ↑↑q
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
h4r : 4 ≤ r
H : 4 ≤ q
⊢ 4 ≤ ↑↑q

q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
h4r : 4 ≤ r
H : 4 ≤ q
⊢ 0 < ↑↑q
assumption_mod_cast
no goals
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
h4r : 4 ≤ r
H : 4 ≤ q
⊢ 0 < ↑↑q
norm_num
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
h4r : 4 ≤ r
H : 4 ≤ q
hq : (↑↑q)⁻¹ ≤ 4⁻¹
⊢ 4 ≤ ↑↑r

q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
h4r : 4 ≤ r
H : 4 ≤ q
hq : (↑↑q)⁻¹ ≤ 4⁻¹
⊢ 0 < ↑↑r
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
h4r : 4 ≤ r
H : 4 ≤ q
hq : (↑↑q)⁻¹ ≤ 4⁻¹
⊢ (↑↑r)⁻¹ ≤ 4⁻¹
rw [inv_le_inv _ h4]
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
h4r : 4 ≤ r
H : 4 ≤ q
hq : (↑↑q)⁻¹ ≤ 4⁻¹
⊢ 0 < ↑↑r
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
h4r : 4 ≤ r
H : 4 ≤ q
hq : (↑↑q)⁻¹ ≤ 4⁻¹
⊢ 4 ≤ ↑↑r

q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
h4r : 4 ≤ r
H : 4 ≤ q
hq : (↑↑q)⁻¹ ≤ 4⁻¹
⊢ 0 < ↑↑r
assumption_mod_cast
no goals
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
h4r : 4 ≤ r
H : 4 ≤ q
hq : (↑↑q)⁻¹ ≤ 4⁻¹
⊢ 0 < ↑↑r
norm_num
no goals
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
h4r : 4 ≤ r
H : 4 ≤ q
hq : (↑↑q)⁻¹ ≤ 4⁻¹
hr : (↑↑r)⁻¹ ≤ 4⁻¹
⊢ 2⁻¹ + 4⁻¹ + 4⁻¹ = 1
norm_num