Theorem ene1

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

	Ref	Expression
Assertion	ene1	⊢ e ≠ 1

Proof

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