Metamath Proof Explorer

Theorem logm1

Description: The natural logarithm of negative 1 . (Contributed by Paul Chapman, 21-Apr-2008) (Revised by Mario Carneiro, 13-May-2014)

Ref Expression
Assertion logm1 
|- ( log ` -u 1 ) = ( _i x. _pi )

Proof

Step Hyp Ref Expression
1 1rp 
 |-  1 e. RR+
2 logneg 
 |-  ( 1 e. RR+ -> ( log ` -u 1 ) = ( ( log ` 1 ) + ( _i x. _pi ) ) )
3 1 2 ax-mp 
 |-  ( log ` -u 1 ) = ( ( log ` 1 ) + ( _i x. _pi ) )
4 log1 
 |-  ( log ` 1 ) = 0
5 4 oveq1i 
 |-  ( ( log ` 1 ) + ( _i x. _pi ) ) = ( 0 + ( _i x. _pi ) )
6 ax-icn 
 |-  _i e. CC
7 picn 
 |-  _pi e. CC
8 6 7 mulcli 
 |-  ( _i x. _pi ) e. CC
9 8 addlidi 
 |-  ( 0 + ( _i x. _pi ) ) = ( _i x. _pi )
10 3 5 9 3eqtri 
 |-  ( log ` -u 1 ) = ( _i x. _pi )