Description: _e is not 1. (Contributed by David A. Wheeler, 17-Oct-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | ene1 | |- _e =/= 1 |
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 |