Theorem ene1

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

	Ref	Expression
Assertion	ene1	$$⊢\mathrm{e}\ne 1$$

Proof

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