This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem epos

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

		Ref	Expression
	Assertion	epos	$⊢ 0 < e$

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