Theorem: logt_gt_one (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
t : ℝ
t_ge : 3 < |t|
⊢ 1 < |t|.log
Tactic:
rw [← Real.log_exp (x := 1)]
State after:
t : ℝ
t_ge : 3 < |t|
⊢ (Real.exp 1).log < |t|.log

State before:
t : ℝ
t_ge : 3 < |t|
⊢ (Real.exp 1).log < |t|.log
Tactic:
apply Real.log_lt_log (Real.exp_pos _)
State after:
t : ℝ
t_ge : 3 < |t|
⊢ Real.exp 1 < |t|

State before:
t : ℝ
t_ge : 3 < |t|
⊢ Real.exp 1 < |t|
Tactic:
linarith [(by exact lt_trans Real.exp_one_lt_d9 (by norm_num) : Real.exp 1 < 3)]
State after:
no goals

State before:
t : ℝ
t_ge : 3 < |t|
⊢ Real.exp 1 < 3
Tactic:
exact lt_trans Real.exp_one_lt_d9 (by norm_num)
State after:
no goals

State before:
t : ℝ
t_ge : 3 < |t|
⊢ 2.7182818286 < 3
Tactic:
norm_num
State after:
no goals