Metamath Proof Explorer

Theorem logdiv2

Description: Generalization of relogdiv to a complex left argument. (Contributed by Mario Carneiro, 8-Jul-2017)

Ref Expression
Assertion logdiv2 
|- ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( log ` ( A / B ) ) = ( ( log ` A ) - ( log ` B ) ) )

Proof

Step Hyp Ref Expression
1 logcl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) e. CC )
2 1 3adant3 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( log ` A ) e. CC )
3 relogcl 
 |-  ( B e. RR+ -> ( log ` B ) e. RR )
4 3 3ad2ant3 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( log ` B ) e. RR )
5 4 recnd 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( log ` B ) e. CC )
6 efsub 
 |-  ( ( ( log ` A ) e. CC /\ ( log ` B ) e. CC ) -> ( exp ` ( ( log ` A ) - ( log ` B ) ) ) = ( ( exp ` ( log ` A ) ) / ( exp ` ( log ` B ) ) ) )
7 2 5 6 syl2anc 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( exp ` ( ( log ` A ) - ( log ` B ) ) ) = ( ( exp ` ( log ` A ) ) / ( exp ` ( log ` B ) ) ) )
8 eflog 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( log ` A ) ) = A )
9 8 3adant3 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( exp ` ( log ` A ) ) = A )
10 reeflog 
 |-  ( B e. RR+ -> ( exp ` ( log ` B ) ) = B )
11 10 3ad2ant3 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( exp ` ( log ` B ) ) = B )
12 9 11 oveq12d 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( ( exp ` ( log ` A ) ) / ( exp ` ( log ` B ) ) ) = ( A / B ) )
13 7 12 eqtrd 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( exp ` ( ( log ` A ) - ( log ` B ) ) ) = ( A / B ) )
14 13 fveq2d 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( log ` ( exp ` ( ( log ` A ) - ( log ` B ) ) ) ) = ( log ` ( A / B ) ) )
15 2 5 negsubd 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( ( log ` A ) + -u ( log ` B ) ) = ( ( log ` A ) - ( log ` B ) ) )
16 logrncl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) e. ran log )
17 16 3adant3 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( log ` A ) e. ran log )
18 4 renegcld 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> -u ( log ` B ) e. RR )
19 logrnaddcl 
 |-  ( ( ( log ` A ) e. ran log /\ -u ( log ` B ) e. RR ) -> ( ( log ` A ) + -u ( log ` B ) ) e. ran log )
20 17 18 19 syl2anc 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( ( log ` A ) + -u ( log ` B ) ) e. ran log )
21 15 20 eqeltrrd 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( ( log ` A ) - ( log ` B ) ) e. ran log )
22 logef 
 |-  ( ( ( log ` A ) - ( log ` B ) ) e. ran log -> ( log ` ( exp ` ( ( log ` A ) - ( log ` B ) ) ) ) = ( ( log ` A ) - ( log ` B ) ) )
23 21 22 syl 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( log ` ( exp ` ( ( log ` A ) - ( log ` B ) ) ) ) = ( ( log ` A ) - ( log ` B ) ) )
24 14 23 eqtr3d 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( log ` ( A / B ) ) = ( ( log ` A ) - ( log ` B ) ) )