Theorem: fourPowLtOf (FromTheBook/Ch02/Bertrand/Bertrand.lean)

State before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 4 ^ n ≤ (4 ^ (n / 3)) ^ 3
Tactic:
rw [← Real.rpow_mul (by norm_num)]
State after:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 4 ^ n ≤ 4 ^ (n / 3 * 3)

State before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 4 ^ n ≤ 4 ^ (n / 3 * 3)
Tactic:
simp
State after:
no goals

State before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 ≤ 4
Tactic:
norm_num
State after:
no goals

State before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ (4 ^ (n / 3)) ^ 3 ≤ ((2 * n) ^ (1 + Real.sqrt (2 * n))) ^ 3
Tactic:
apply Real.rpow_le_rpow _ h (by linarith)
State after:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 ≤ 4 ^ (n / 3)

State before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 ≤ 4 ^ (n / 3)
Tactic:
apply Real.rpow_nonneg_of_nonneg (by norm_num)
State after:
no goals

State before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 ≤ 3
Tactic:
linarith
State after:
no goals

State before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ ((2 * n) ^ (1 + Real.sqrt (2 * n))) ^ 3 = (2 * n) ^ ((1 + Real.sqrt (2 * n)) * 3)
Tactic:
rw [Real.rpow_mul (by linarith)]
State after:
no goals

State before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 ≤ 2 * n
Tactic:
linarith
State after:
no goals

State before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ (2 * n) ^ ((1 + Real.sqrt (2 * n)) * 3) < (2 ^ (6 * (2 * n) ^ 6⁻¹)) ^ ((1 + Real.sqrt (2 * n)) * 3)
Tactic:
apply Real.rpow_lt_rpow (by linarith) (twoMulLtTwoPow (by linarith))
State after:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 < (1 + Real.sqrt (2 * n)) * 3

State before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 < (1 + Real.sqrt (2 * n)) * 3
Tactic:
simp
State after:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 < 1 + Real.sqrt (2 * n)

State before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 < 1 + Real.sqrt (2 * n)
Tactic:
exact lt_add_of_pos_of_le (by norm_num) (Real.sqrt_nonneg _)
State after:
no goals

State before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 32 ≤ n
Tactic:
linarith
State after:
no goals

State before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 < 1
Tactic:
norm_num
State after:
no goals

State before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ (2 ^ (6 * (2 * n) ^ 6⁻¹)) ^ ((1 + Real.sqrt (2 * n)) * 3) < 2 ^ (20 * (2 * n) ^ (2 / 3))
Tactic:
rw [← Real.rpow_mul (by linarith)]
State after:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 2 ^ (6 * (2 * n) ^ 6⁻¹ * ((1 + Real.sqrt (2 * n)) * 3)) < 2 ^ (20 * (2 * n) ^ (2 / 3))

State before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 2 ^ (6 * (2 * n) ^ 6⁻¹ * ((1 + Real.sqrt (2 * n)) * 3)) < 2 ^ (20 * (2 * n) ^ (2 / 3))
Tactic:
rw [Real.rpow_lt_rpow_left_iff (by linarith)]
State after:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 6 * (2 * n) ^ 6⁻¹ * ((1 + Real.sqrt (2 * n)) * 3) < 20 * (2 * n) ^ (2 / 3)

State before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 6 * (2 * n) ^ 6⁻¹ * ((1 + Real.sqrt (2 * n)) * 3) < 20 * (2 * n) ^ (2 / 3)
Tactic:
calc
_ = (18 * (1 + Real.sqrt (2*n))) * ((2*n)^6⁻¹) := by linarith
_ < (2 + 18) * Real.sqrt (2*n) * (2*n)^6⁻¹ := by
  rw [mul_lt_mul_right]
  . simp [mul_add, add_mul]
    apply ltTwoMulSqrtTwoMul
    linarith
  . apply Real.rpow_pos_of_pos
    linarith
_ = 20 * (Real.sqrt (2*n) * (2*n)^6⁻¹) := by linarith
_ = _ := by
  simp [Real.sqrt_eq_rpow]
  rw [← Real.rpow_add (by linarith)]
  norm_num
State after:
no goals

State before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 ≤ 2
Tactic:
linarith
State after:
no goals

State before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 1 < 2
Tactic:
linarith
State after:
no goals

State before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 6 * (2 * n) ^ 6⁻¹ * ((1 + Real.sqrt (2 * n)) * 3) = 18 * (1 + Real.sqrt (2 * n)) * (2 * n) ^ 6⁻¹
Tactic:
linarith
State after:
no goals

State before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 18 * (1 + Real.sqrt (2 * n)) * (2 * n) ^ 6⁻¹ < (2 + 18) * Real.sqrt (2 * n) * (2 * n) ^ 6⁻¹
Tactic:
rw [mul_lt_mul_right]
State after:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 18 * (1 + Real.sqrt (2 * n)) < (2 + 18) * Real.sqrt (2 * n)

n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 < (2 * n) ^ 6⁻¹

State before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 18 * (1 + Real.sqrt (2 * n)) < (2 + 18) * Real.sqrt (2 * n)

n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 < (2 * n) ^ 6⁻¹
Tactic:
. simp [mul_add, add_mul]
  apply ltTwoMulSqrtTwoMul
  linarith
State after:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 < (2 * n) ^ 6⁻¹

State before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 < (2 * n) ^ 6⁻¹
Tactic:
. apply Real.rpow_pos_of_pos
  linarith
State after:
no goals

State before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 18 * (1 + Real.sqrt (2 * n)) < (2 + 18) * Real.sqrt (2 * n)
Tactic:
simp [mul_add, add_mul]
State after:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 18 < 2 * Real.sqrt (2 * n)

State before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 18 < 2 * Real.sqrt (2 * n)
Tactic:
apply ltTwoMulSqrtTwoMul
State after:
case h
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 81 / 2 < n

State before:
case h
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 81 / 2 < n
Tactic:
linarith
State after:
no goals

State before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 < (2 * n) ^ 6⁻¹
Tactic:
apply Real.rpow_pos_of_pos
State after:
case hx
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 < 2 * n

State before:
case hx
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 < 2 * n
Tactic:
linarith
State after:
no goals

State before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ (2 + 18) * Real.sqrt (2 * n) * (2 * n) ^ 6⁻¹ = 20 * (Real.sqrt (2 * n) * (2 * n) ^ 6⁻¹)
Tactic:
linarith
State after:
no goals

State before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 20 * (Real.sqrt (2 * n) * (2 * n) ^ 6⁻¹) = 20 * (2 * n) ^ (2 / 3)
Tactic:
simp [Real.sqrt_eq_rpow]
State after:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ (2 * n) ^ 2⁻¹ * (2 * n) ^ 6⁻¹ = (2 * n) ^ (2 / 3)

State before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ (2 * n) ^ 2⁻¹ * (2 * n) ^ 6⁻¹ = (2 * n) ^ (2 / 3)
Tactic:
rw [← Real.rpow_add (by linarith)]
State after:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ (2 * n) ^ (2⁻¹ + 6⁻¹) = (2 * n) ^ (2 / 3)

State before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ (2 * n) ^ (2⁻¹ + 6⁻¹) = (2 * n) ^ (2 / 3)
Tactic:
norm_num
State after:
no goals

State before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 < 2 * n
Tactic:
linarith
State after:
no goals