Metamath Proof Explorer


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 e. RR
2 1lt2
 |-  1 < 2
3 egt2lt3
 |-  ( 2 < _e /\ _e < 3 )
4 3 simpli
 |-  2 < _e
5 2re
 |-  2 e. RR
6 ere
 |-  _e e. RR
7 1 5 6 lttri
 |-  ( ( 1 < 2 /\ 2 < _e ) -> 1 < _e )
8 2 4 7 mp2an
 |-  1 < _e
9 1 8 gtneii
 |-  _e =/= 1