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

Metamath Proof Explorer

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