theorem proved term proof

`e_gt_two`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 163theorem e_gt_two : Real.exp 1 > 2 := by

Term-mode proof.

 164  have h := Real.add_one_lt_exp (show (1:ℝ) ≠ 0 by norm_num)
 165  linarith
 166
 167/-- φ < 2 (from phi < 1.62). -/

From the project-wide theorem graph. These declarations reference this one in their body.

Lean names referenced from this declaration's body.