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

p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
h3q : 3 ≤ q
h3r : 3 ≤ r
H : 3 ≤ p
⊢ 0 < ↑↑p
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
h3q : 3 ≤ q
h3r : 3 ≤ r
H : 3 ≤ p
⊢ (↑↑p)⁻¹ ≤ 3⁻¹
rw [inv_le_inv _ h3]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
h3q : 3 ≤ q
h3r : 3 ≤ r
H : 3 ≤ p
⊢ 0 < ↑↑p
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
h3q : 3 ≤ q
h3r : 3 ≤ r
H : 3 ≤ p
⊢ 3 ≤ ↑↑p

p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
h3q : 3 ≤ q
h3r : 3 ≤ r
H : 3 ≤ p
⊢ 0 < ↑↑p
assumption_mod_cast
no goals
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
h3q : 3 ≤ q
h3r : 3 ≤ r
H : 3 ≤ p
⊢ 0 < ↑↑p
norm_num
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
h3q : 3 ≤ q
h3r : 3 ≤ r
H : 3 ≤ p
hp : (↑↑p)⁻¹ ≤ 3⁻¹
⊢ 3 ≤ ↑↑q

p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
h3q : 3 ≤ q
h3r : 3 ≤ r
H : 3 ≤ p
hp : (↑↑p)⁻¹ ≤ 3⁻¹
⊢ 0 < ↑↑q
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
h3q : 3 ≤ q
h3r : 3 ≤ r
H : 3 ≤ p
hp : (↑↑p)⁻¹ ≤ 3⁻¹
⊢ (↑↑q)⁻¹ ≤ 3⁻¹
rw [inv_le_inv _ h3]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
h3q : 3 ≤ q
h3r : 3 ≤ r
H : 3 ≤ p
hp : (↑↑p)⁻¹ ≤ 3⁻¹
⊢ 0 < ↑↑q
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
h3q : 3 ≤ q
h3r : 3 ≤ r
H : 3 ≤ p
hp : (↑↑p)⁻¹ ≤ 3⁻¹
⊢ 3 ≤ ↑↑q

p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
h3q : 3 ≤ q
h3r : 3 ≤ r
H : 3 ≤ p
hp : (↑↑p)⁻¹ ≤ 3⁻¹
⊢ 0 < ↑↑q
assumption_mod_cast
no goals
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
h3q : 3 ≤ q
h3r : 3 ≤ r
H : 3 ≤ p
hp : (↑↑p)⁻¹ ≤ 3⁻¹
⊢ 0 < ↑↑q
norm_num
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
h3q : 3 ≤ q
h3r : 3 ≤ r
H : 3 ≤ p
hp : (↑↑p)⁻¹ ≤ 3⁻¹
hq : (↑↑q)⁻¹ ≤ 3⁻¹
⊢ 3 ≤ ↑↑r

p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
h3q : 3 ≤ q
h3r : 3 ≤ r
H : 3 ≤ p
hp : (↑↑p)⁻¹ ≤ 3⁻¹
hq : (↑↑q)⁻¹ ≤ 3⁻¹
⊢ 0 < ↑↑r
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
h3q : 3 ≤ q
h3r : 3 ≤ r
H : 3 ≤ p
hp : (↑↑p)⁻¹ ≤ 3⁻¹
hq : (↑↑q)⁻¹ ≤ 3⁻¹
⊢ (↑↑r)⁻¹ ≤ 3⁻¹
rw [inv_le_inv _ h3]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
h3q : 3 ≤ q
h3r : 3 ≤ r
H : 3 ≤ p
hp : (↑↑p)⁻¹ ≤ 3⁻¹
hq : (↑↑q)⁻¹ ≤ 3⁻¹
⊢ 0 < ↑↑r
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
h3q : 3 ≤ q
h3r : 3 ≤ r
H : 3 ≤ p
hp : (↑↑p)⁻¹ ≤ 3⁻¹
hq : (↑↑q)⁻¹ ≤ 3⁻¹
⊢ 3 ≤ ↑↑r

p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
h3q : 3 ≤ q
h3r : 3 ≤ r
H : 3 ≤ p
hp : (↑↑p)⁻¹ ≤ 3⁻¹
hq : (↑↑q)⁻¹ ≤ 3⁻¹
⊢ 0 < ↑↑r
assumption_mod_cast
no goals
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
h3q : 3 ≤ q
h3r : 3 ≤ r
H : 3 ≤ p
hp : (↑↑p)⁻¹ ≤ 3⁻¹
hq : (↑↑q)⁻¹ ≤ 3⁻¹
⊢ 0 < ↑↑r
norm_num
no goals
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
h3q : 3 ≤ q
h3r : 3 ≤ r
H : 3 ≤ p
hp : (↑↑p)⁻¹ ≤ 3⁻¹
hq : (↑↑q)⁻¹ ≤ 3⁻¹
hr : (↑↑r)⁻¹ ≤ 3⁻¹
⊢ 3⁻¹ + 3⁻¹ + 3⁻¹ = 1
norm_num