Theorem: UpperBnd_aux2 (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
A σ t : ℝ
t_ge : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
⊢ |t| ^ (1 - σ) ≤ A.exp
Tactic:
have : |t| ^ (1 - σ) ≤ |t| ^ (A / Real.log |t|) :=
  Real.rpow_le_rpow_of_exponent_le (by linarith) (by linarith)
State after:
A σ t : ℝ
t_ge : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
this : |t| ^ (1 - σ) ≤ |t| ^ (A / |t|.log)
⊢ |t| ^ (1 - σ) ≤ A.exp

State before:
A σ t : ℝ
t_ge : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
this : |t| ^ (1 - σ) ≤ |t| ^ (A / |t|.log)
⊢ |t| ^ (1 - σ) ≤ A.exp
Tactic:
apply le_trans this ?_
State after:
A σ t : ℝ
t_ge : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
this : |t| ^ (1 - σ) ≤ |t| ^ (A / |t|.log)
⊢ |t| ^ (A / |t|.log) ≤ A.exp

State before:
A σ t : ℝ
t_ge : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
this : |t| ^ (1 - σ) ≤ |t| ^ (A / |t|.log)
⊢ |t| ^ (A / |t|.log) ≤ A.exp
Tactic:
conv => lhs; lhs; rw [← Real.exp_log (by linarith : 0 < |t|)]
State after:
A σ t : ℝ
t_ge : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
this : |t| ^ (1 - σ) ≤ |t| ^ (A / |t|.log)
⊢ |t|.log.exp ^ (A / |t|.log) ≤ A.exp

State before:
A σ t : ℝ
t_ge : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
this : |t| ^ (1 - σ) ≤ |t| ^ (A / |t|.log)
⊢ |t|.log.exp ^ (A / |t|.log) ≤ A.exp
Tactic:
rw [div_eq_mul_inv, Real.rpow_mul (by positivity), ← Real.exp_mul, ← Real.exp_mul, mul_comm,
  ← mul_assoc, inv_mul_cancel, one_mul]
State after:
A σ t : ℝ
t_ge : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
this : |t| ^ (1 - σ) ≤ |t| ^ (A / |t|.log)
⊢ |t|.log ≠ 0

State before:
A σ t : ℝ
t_ge : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
this : |t| ^ (1 - σ) ≤ |t| ^ (A / |t|.log)
⊢ |t|.log ≠ 0
Tactic:
apply Real.log_ne_zero.mpr
State after:
A σ t : ℝ
t_ge : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
this : |t| ^ (1 - σ) ≤ |t| ^ (A / |t|.log)
⊢ |t| ≠ 0 ∧ |t| ≠ 1 ∧ |t| ≠ -1

State before:
A σ t : ℝ
t_ge : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
this : |t| ^ (1 - σ) ≤ |t| ^ (A / |t|.log)
⊢ |t| ≠ 0 ∧ |t| ≠ 1 ∧ |t| ≠ -1
Tactic:
split_ands <;> linarith
State after:
no goals

State before:
A σ t : ℝ
t_ge : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
⊢ 1 ≤ |t|
Tactic:
linarith
State after:
no goals

State before:
A σ t : ℝ
t_ge : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
⊢ 1 - σ ≤ A / |t|.log
Tactic:
linarith
State after:
no goals

State before:
A σ t : ℝ
t_ge : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
this : |t| ^ (1 - σ) ≤ |t| ^ (A / |t|.log)
⊢ 0 < |t|
Tactic:
linarith
State after:
no goals

State before:
A σ t : ℝ
t_ge : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
this : |t| ^ (1 - σ) ≤ |t| ^ (A / |t|.log)
⊢ 0 ≤ |t|.log.exp
Tactic:
positivity
State after:
no goals