Lower bound for real exponential

Stream: new members

[Joan Domingo Pasarin]

Quick question. How does one prove that exp 7 \ge 2 ^ 9? I tried using norm_num but the tactic only converts the goal to 512 \le rexp 7. I also tried linarith which didn't work either.

[Ruben Van de Velde]

norm_num is the right answer, but perhaps not today

[Aaron Liu]

import Mathlib

open Real
example : exp 7 ≥ 2 ^ 9 := by
  have h : exp 1 ^ 7 = exp 7 := by simp
  rw [← h]
  refine le_trans ?_ (pow_le_pow_left₀ (by norm_num) Real.exp_one_gt_d9.le 7)
  norm_num

[Joan Domingo Pasarin]

I see, thank you!

[Yiming Fu]

This might help. LeanCert