theorem
proved
tactic proof
e_in_eInterval
show as:
view Lean formalization →
formal statement (Lean)
79theorem e_in_eInterval : eInterval.contains (exp 1) := by
proof body
Tactic-mode proof.
80 simp only [Interval.contains, eInterval]
81 constructor
82 · -- 2.718 ≤ exp(1)
83 have h := Real.exp_one_gt_d9 -- 2.7182818283 < exp 1
84 have h1 : ((2718 / 1000 : ℚ) : ℝ) = (2.718 : ℝ) := by norm_num
85 linarith
86 · -- exp(1) ≤ 2.719
87 have h := Real.exp_one_lt_d9 -- exp 1 < 2.7182818286
88 have h1 : ((2719 / 1000 : ℚ) : ℝ) = (2.719 : ℝ) := by norm_num
89 linarith
90
91end IndisputableMonolith.Numerics