Theorem epos

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

	Ref	Expression
Assertion	epos	$$⊢0<\mathrm{e}$$

Proof

Step	Hyp	Ref	Expression
1		2pos	$$⊢0<2$$
2		egt2lt3	$$⊢\left(2<\mathrm{e}\wedge \mathrm{e}<3\right)$$
3	2	simpli	$$⊢2<\mathrm{e}$$
4		0re	$$⊢0\in ℝ$$
5		2re	$$⊢2\in ℝ$$
6		ere	$$⊢\mathrm{e}\in ℝ$$
7	4 5 6	lttri	$$⊢\left(0<2\wedge 2<\mathrm{e}\right)\to 0<\mathrm{e}$$
8	1 3 7	mp2an	$$⊢0<\mathrm{e}$$