Metamath Proof Explorer
Description: The natural logarithm of 1 . One case of Property 1a of Cohen
p. 301. (Contributed by Steve Rodriguez, 25Nov2007)


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 