This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cxpmul

Description: Product of exponents law for complex exponentiation. Proposition 10-4.2(b) of Gleason p. 135. (Contributed by Mario Carneiro, 2-Aug-2014)

Ref Expression
Assertion cxpmul 
|- ( ( A e. RR+ /\ B e. RR /\ C e. CC ) -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^c C ) )

Proof

Step Hyp Ref Expression
1 simp3 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. CC ) -> C e. CC )
2 simp2 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. CC ) -> B e. RR )
3 2 recnd 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. CC ) -> B e. CC )
4 relogcl 
 |-  ( A e. RR+ -> ( log ` A ) e. RR )
5 4 3ad2ant1 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. CC ) -> ( log ` A ) e. RR )
6 5 recnd 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. CC ) -> ( log ` A ) e. CC )
7 1 3 6 mulassd 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. CC ) -> ( ( C x. B ) x. ( log ` A ) ) = ( C x. ( B x. ( log ` A ) ) ) )
8 3 1 mulcomd 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. CC ) -> ( B x. C ) = ( C x. B ) )
9 8 oveq1d 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. CC ) -> ( ( B x. C ) x. ( log ` A ) ) = ( ( C x. B ) x. ( log ` A ) ) )
10 rpcn 
 |-  ( A e. RR+ -> A e. CC )
11 10 3ad2ant1 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. CC ) -> A e. CC )
12 rpne0 
 |-  ( A e. RR+ -> A =/= 0 )
13 12 3ad2ant1 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. CC ) -> A =/= 0 )
14 cxpef 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> ( A ^c B ) = ( exp ` ( B x. ( log ` A ) ) ) )
15 11 13 3 14 syl3anc 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. CC ) -> ( A ^c B ) = ( exp ` ( B x. ( log ` A ) ) ) )
16 15 fveq2d 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. CC ) -> ( log ` ( A ^c B ) ) = ( log ` ( exp ` ( B x. ( log ` A ) ) ) ) )
17 2 5 remulcld 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. CC ) -> ( B x. ( log ` A ) ) e. RR )
18 17 relogefd 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. CC ) -> ( log ` ( exp ` ( B x. ( log ` A ) ) ) ) = ( B x. ( log ` A ) ) )
19 16 18 eqtrd 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. CC ) -> ( log ` ( A ^c B ) ) = ( B x. ( log ` A ) ) )
20 19 oveq2d 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. CC ) -> ( C x. ( log ` ( A ^c B ) ) ) = ( C x. ( B x. ( log ` A ) ) ) )
21 7 9 20 3eqtr4d 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. CC ) -> ( ( B x. C ) x. ( log ` A ) ) = ( C x. ( log ` ( A ^c B ) ) ) )
22 21 fveq2d 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. CC ) -> ( exp ` ( ( B x. C ) x. ( log ` A ) ) ) = ( exp ` ( C x. ( log ` ( A ^c B ) ) ) ) )
23 3 1 mulcld 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. CC ) -> ( B x. C ) e. CC )
24 cxpef 
 |-  ( ( A e. CC /\ A =/= 0 /\ ( B x. C ) e. CC ) -> ( A ^c ( B x. C ) ) = ( exp ` ( ( B x. C ) x. ( log ` A ) ) ) )
25 11 13 23 24 syl3anc 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. CC ) -> ( A ^c ( B x. C ) ) = ( exp ` ( ( B x. C ) x. ( log ` A ) ) ) )
26 cxpcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A ^c B ) e. CC )
27 11 3 26 syl2anc 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. CC ) -> ( A ^c B ) e. CC )
28 cxpne0 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> ( A ^c B ) =/= 0 )
29 11 13 3 28 syl3anc 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. CC ) -> ( A ^c B ) =/= 0 )
30 cxpef 
 |-  ( ( ( A ^c B ) e. CC /\ ( A ^c B ) =/= 0 /\ C e. CC ) -> ( ( A ^c B ) ^c C ) = ( exp ` ( C x. ( log ` ( A ^c B ) ) ) ) )
31 27 29 1 30 syl3anc 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. CC ) -> ( ( A ^c B ) ^c C ) = ( exp ` ( C x. ( log ` ( A ^c B ) ) ) ) )
32 22 25 31 3eqtr4d 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. CC ) -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^c C ) )