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

Metamath Proof Explorer

Theorem ene1

Description: _e is not 1. (Contributed by David A. Wheeler, 17-Oct-2017)

		Ref	Expression
	Assertion	ene1	$⊢ e \neq 1$

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