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