Theorem log1

Description: The natural logarithm of 1 . One case of Property 1a of Cohen p. 301. (Contributed by Steve Rodriguez, 25-Nov-2007)

	Ref	Expression
Assertion	log1	⊢ ( log ‘ 1 ) = 0

Proof

Step	Hyp	Ref	Expression
1		ef0	⊢ ( exp ‘ 0 ) = 1
2		1rp	⊢ 1 ∈ ℝ+
3		0re	⊢ 0 ∈ ℝ
4		relogeftb	⊢ ( ( 1 ∈ ℝ+ ∧ 0 ∈ ℝ ) → ( ( log ‘ 1 ) = 0 ↔ ( exp ‘ 0 ) = 1 ) )
5	2 3 4	mp2an	⊢ ( ( log ‘ 1 ) = 0 ↔ ( exp ‘ 0 ) = 1 )
6	1 5	mpbir	⊢ ( log ‘ 1 ) = 0