This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem loge

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

Proof

Step Hyp Ref Expression
1 df-e ⊢ e = ( exp ‘ 1 )
2 1 eqcomi ⊢ ( exp ‘ 1 ) = e
3 epr ⊢ e ∈ ℝ+
4 1re ⊢ 1 ∈ ℝ
5 relogeftb ⊢ ( ( e ∈ ℝ+ ∧ 1 ∈ ℝ ) → ( ( log ‘ e ) = 1 ↔ ( exp ‘ 1 ) = e ) )
6 3 4 5 mp2an ⊢ ( ( log ‘ e ) = 1 ↔ ( exp ‘ 1 ) = e )
7 2 6 mpbir ⊢ ( log ‘ e ) = 1