lemma
proved
tactic proof
exp_463407156_upper
show as:
view Lean formalization →
formal statement (Lean)
477private lemma exp_463407156_upper : Real.exp (4.63407156 : ℝ) < (103 : ℝ) := by
proof body
Tactic-mode proof.
478 have hsplit : Real.exp (4.63407156 : ℝ) = Real.exp (4 : ℝ) * Real.exp (0.63407156 : ℝ) := by
479 have h : (4.63407156 : ℝ) = (4 : ℝ) + (0.63407156 : ℝ) := by norm_num
480 rw [h, Real.exp_add]
481 rw [hsplit]
482 have h1 : Real.exp (4 : ℝ) < (54.598151 : ℝ) := exp_four_upper
483 have h2 : Real.exp (0.63407156 : ℝ) < (1.88528 : ℝ) := exp_063407156_upper
484 have hprod : Real.exp (4 : ℝ) * Real.exp (0.63407156 : ℝ) <
485 (54.598151 : ℝ) * (1.88528 : ℝ) := by
486 nlinarith [h1, h2, Real.exp_pos (4 : ℝ), Real.exp_pos (0.63407156 : ℝ)]
487 have hnum : (54.598151 : ℝ) * (1.88528 : ℝ) < (103 : ℝ) := by norm_num
488 exact lt_trans hprod hnum
489