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 |