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 ) ) )