theorem
proved
e_pos
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Mathematics.Euler on GitHub at line 160.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
157/-! ## Provable Bounds on e and φ -/
158
159/-- e = exp(1) is positive. -/
160theorem e_pos : Real.exp 1 > 0 := Real.exp_pos 1
161
162/-- e > 2 (from the strict convexity of exp, or 1+x < exp(x) for x ≠ 0). -/
163theorem e_gt_two : Real.exp 1 > 2 := by
164 have h := Real.add_one_lt_exp (show (1:ℝ) ≠ 0 by norm_num)
165 linarith
166
167/-- φ < 2 (from phi < 1.62). -/
168theorem phi_lt_two : phi < 2 := by
169 linarith [Constants.phi_lt_onePointSixTwo]
170
171/-- e > φ: Euler's number exceeds the golden ratio. -/
172theorem e_gt_phi : phi < Real.exp 1 := by
173 have h1 : phi < 2 := phi_lt_two
174 have h2 : Real.exp 1 > 2 := e_gt_two
175 linarith
176
177/-- e ≠ φ: e and φ are distinct constants. -/
178theorem e_ne_phi : Real.exp 1 ≠ phi := ne_of_gt e_gt_phi
179
180/-- e > 1: e exceeds 1. -/
181theorem e_gt_one : Real.exp 1 > 1 := by
182 linarith [e_gt_two]
183
184/-! ## φ and e: A Deeper Connection? -/
185
186/-- Is there a deep connection between φ and e?
187
188 Both are transcendental.
189 Both appear in growth processes.
190