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 e. RR+
3 0re 
 |-  0 e. RR
4 relogeftb 
 |-  ( ( 1 e. RR+ /\ 0 e. RR ) -> ( ( log ` 1 ) = 0 <-> ( exp ` 0 ) = 1 ) )
5 2 3 4 mp2an 
 |-  ( ( log ` 1 ) = 0 <-> ( exp ` 0 ) = 1 )
6 1 5 mpbir 
 |-  ( log ` 1 ) = 0