Metamath Proof Explorer

Theorem logmul2

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

Ref Expression
Assertion logmul2 
|- ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( log ` ( A x. 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 efadd 
 |-  ( ( ( log ` A ) e. CC /\ ( log ` B ) e. CC ) -> ( exp ` ( ( log ` A ) + ( log ` B ) ) ) = ( ( exp ` ( log ` A ) ) x. ( exp ` ( log ` B ) ) ) )
7 2 5 6 syl2anc 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( exp ` ( ( log ` A ) + ( log ` B ) ) ) = ( ( exp ` ( log ` A ) ) x. ( 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 ) ) x. ( exp ` ( log ` B ) ) ) = ( A x. B ) )
13 7 12 eqtrd 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( exp ` ( ( log ` A ) + ( log ` B ) ) ) = ( A x. B ) )
14 13 fveq2d 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( log ` ( exp ` ( ( log ` A ) + ( log ` B ) ) ) ) = ( log ` ( A x. B ) ) )
15 logrncl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) e. ran log )
16 15 3adant3 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( log ` A ) e. ran log )
17 logrnaddcl 
 |-  ( ( ( log ` A ) e. ran log /\ ( log ` B ) e. RR ) -> ( ( log ` A ) + ( log ` B ) ) e. ran log )
18 16 4 17 syl2anc 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( ( log ` A ) + ( log ` B ) ) e. ran log )
19 logef 
 |-  ( ( ( log ` A ) + ( log ` B ) ) e. ran log -> ( log ` ( exp ` ( ( log ` A ) + ( log ` B ) ) ) ) = ( ( log ` A ) + ( log ` B ) ) )
20 18 19 syl 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( log ` ( exp ` ( ( log ` A ) + ( log ` B ) ) ) ) = ( ( log ` A ) + ( log ` B ) ) )
21 14 20 eqtr3d 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( log ` ( A x. B ) ) = ( ( log ` A ) + ( log ` B ) ) )