Description: The natural logarithm of _e . One case of Property 1b of Cohen p. 301. (Contributed by Steve Rodriguez, 25-Nov-2007)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | loge | |- ( log ` _e ) = 1 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-e | |- _e = ( exp ` 1 ) |
|
| 2 | 1 | eqcomi | |- ( exp ` 1 ) = _e |
| 3 | epr | |- _e e. RR+ |
|
| 4 | 1re | |- 1 e. RR |
|
| 5 | relogeftb | |- ( ( _e e. RR+ /\ 1 e. RR ) -> ( ( log ` _e ) = 1 <-> ( exp ` 1 ) = _e ) ) |
|
| 6 | 3 4 5 | mp2an | |- ( ( log ` _e ) = 1 <-> ( exp ` 1 ) = _e ) |
| 7 | 2 6 | mpbir | |- ( log ` _e ) = 1 |