Theorem epos

Description: Euler's constant _e is greater than 0. (Contributed by Jeff Hankins, 22-Nov-2008)

	Ref	Expression
Assertion	epos	⊢ 0 < e

Proof

Step	Hyp	Ref	Expression
1		2pos	⊢ 0 < 2
2		egt2lt3	⊢ ( 2 < e ∧ e < 3 )
3	2	simpli	⊢ 2 < e
4		0re	⊢ 0 ∈ ℝ
5		2re	⊢ 2 ∈ ℝ
6		ere	⊢ e ∈ ℝ
7	4 5 6	lttri	⊢ ( ( 0 < 2 ∧ 2 < e ) → 0 < e )
8	1 3 7	mp2an	⊢ 0 < e