theorem proved term proof

`e_ne_phi`

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

formal statement (Lean)

 178theorem e_ne_phi : Real.exp 1 ≠ phi := ne_of_gt e_gt_phi

Term-mode proof.

 179
 180/-- e > 1: e exceeds 1. -/

Lean names referenced from this declaration's body.