Metamath Proof Explorer

Theorem mulcxp

Description: Complex exponentiation of a product. Proposition 10-4.2(c) of Gleason p. 135. (Contributed by Mario Carneiro, 2-Aug-2014)

Ref Expression
Assertion mulcxp 
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) -> ( ( A x. B ) ^c C ) = ( ( A ^c C ) x. ( B ^c C ) ) )

Proof

Step Hyp Ref Expression
1 simp1l 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) -> A e. RR )
2 1 recnd 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) -> A e. CC )
3 2 mul01d 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) -> ( A x. 0 ) = 0 )
4 3 oveq1d 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) -> ( ( A x. 0 ) ^c C ) = ( 0 ^c C ) )
5 simp3 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) -> C e. CC )
6 2 5 mulcxplem 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) -> ( 0 ^c C ) = ( ( A ^c C ) x. ( 0 ^c C ) ) )
7 4 6 eqtrd 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) -> ( ( A x. 0 ) ^c C ) = ( ( A ^c C ) x. ( 0 ^c C ) ) )
8 oveq2 
 |-  ( B = 0 -> ( A x. B ) = ( A x. 0 ) )
9 8 oveq1d 
 |-  ( B = 0 -> ( ( A x. B ) ^c C ) = ( ( A x. 0 ) ^c C ) )
10 oveq1 
 |-  ( B = 0 -> ( B ^c C ) = ( 0 ^c C ) )
11 10 oveq2d 
 |-  ( B = 0 -> ( ( A ^c C ) x. ( B ^c C ) ) = ( ( A ^c C ) x. ( 0 ^c C ) ) )
12 9 11 eqeq12d 
 |-  ( B = 0 -> ( ( ( A x. B ) ^c C ) = ( ( A ^c C ) x. ( B ^c C ) ) <-> ( ( A x. 0 ) ^c C ) = ( ( A ^c C ) x. ( 0 ^c C ) ) ) )
13 7 12 syl5ibrcom 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) -> ( B = 0 -> ( ( A x. B ) ^c C ) = ( ( A ^c C ) x. ( B ^c C ) ) ) )
14 simp2l 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) -> B e. RR )
15 14 recnd 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) -> B e. CC )
16 15 mul02d 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) -> ( 0 x. B ) = 0 )
17 16 oveq1d 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) -> ( ( 0 x. B ) ^c C ) = ( 0 ^c C ) )
18 15 5 mulcxplem 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) -> ( 0 ^c C ) = ( ( B ^c C ) x. ( 0 ^c C ) ) )
19 cxpcl 
 |-  ( ( B e. CC /\ C e. CC ) -> ( B ^c C ) e. CC )
20 15 5 19 syl2anc 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) -> ( B ^c C ) e. CC )
21 0cn 
 |-  0 e. CC
22 cxpcl 
 |-  ( ( 0 e. CC /\ C e. CC ) -> ( 0 ^c C ) e. CC )
23 21 5 22 sylancr 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) -> ( 0 ^c C ) e. CC )
24 20 23 mulcomd 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) -> ( ( B ^c C ) x. ( 0 ^c C ) ) = ( ( 0 ^c C ) x. ( B ^c C ) ) )
25 18 24 eqtrd 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) -> ( 0 ^c C ) = ( ( 0 ^c C ) x. ( B ^c C ) ) )
26 17 25 eqtrd 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) -> ( ( 0 x. B ) ^c C ) = ( ( 0 ^c C ) x. ( B ^c C ) ) )
27 oveq1 
 |-  ( A = 0 -> ( A x. B ) = ( 0 x. B ) )
28 27 oveq1d 
 |-  ( A = 0 -> ( ( A x. B ) ^c C ) = ( ( 0 x. B ) ^c C ) )
29 oveq1 
 |-  ( A = 0 -> ( A ^c C ) = ( 0 ^c C ) )
30 29 oveq1d 
 |-  ( A = 0 -> ( ( A ^c C ) x. ( B ^c C ) ) = ( ( 0 ^c C ) x. ( B ^c C ) ) )
31 28 30 eqeq12d 
 |-  ( A = 0 -> ( ( ( A x. B ) ^c C ) = ( ( A ^c C ) x. ( B ^c C ) ) <-> ( ( 0 x. B ) ^c C ) = ( ( 0 ^c C ) x. ( B ^c C ) ) ) )
32 26 31 syl5ibrcom 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) -> ( A = 0 -> ( ( A x. B ) ^c C ) = ( ( A ^c C ) x. ( B ^c C ) ) ) )
33 32 a1dd 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) -> ( A = 0 -> ( B =/= 0 -> ( ( A x. B ) ^c C ) = ( ( A ^c C ) x. ( B ^c C ) ) ) ) )
34 1 adantr 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> A e. RR )
35 simpl1r 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> 0 <_ A )
36 simprl 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> A =/= 0 )
37 34 35 36 ne0gt0d 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> 0 < A )
38 34 37 elrpd 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> A e. RR+ )
39 14 adantr 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> B e. RR )
40 simpl2r 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> 0 <_ B )
41 simprr 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> B =/= 0 )
42 39 40 41 ne0gt0d 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> 0 < B )
43 39 42 elrpd 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> B e. RR+ )
44 38 43 relogmuld 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> ( log ` ( A x. B ) ) = ( ( log ` A ) + ( log ` B ) ) )
45 44 oveq2d 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> ( C x. ( log ` ( A x. B ) ) ) = ( C x. ( ( log ` A ) + ( log ` B ) ) ) )
46 5 adantr 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> C e. CC )
47 2 adantr 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> A e. CC )
48 47 36 logcld 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> ( log ` A ) e. CC )
49 15 adantr 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> B e. CC )
50 49 41 logcld 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> ( log ` B ) e. CC )
51 46 48 50 adddid 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> ( C x. ( ( log ` A ) + ( log ` B ) ) ) = ( ( C x. ( log ` A ) ) + ( C x. ( log ` B ) ) ) )
52 45 51 eqtrd 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> ( C x. ( log ` ( A x. B ) ) ) = ( ( C x. ( log ` A ) ) + ( C x. ( log ` B ) ) ) )
53 52 fveq2d 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> ( exp ` ( C x. ( log ` ( A x. B ) ) ) ) = ( exp ` ( ( C x. ( log ` A ) ) + ( C x. ( log ` B ) ) ) ) )
54 46 48 mulcld 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> ( C x. ( log ` A ) ) e. CC )
55 46 50 mulcld 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> ( C x. ( log ` B ) ) e. CC )
56 efadd 
 |-  ( ( ( C x. ( log ` A ) ) e. CC /\ ( C x. ( log ` B ) ) e. CC ) -> ( exp ` ( ( C x. ( log ` A ) ) + ( C x. ( log ` B ) ) ) ) = ( ( exp ` ( C x. ( log ` A ) ) ) x. ( exp ` ( C x. ( log ` B ) ) ) ) )
57 54 55 56 syl2anc 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> ( exp ` ( ( C x. ( log ` A ) ) + ( C x. ( log ` B ) ) ) ) = ( ( exp ` ( C x. ( log ` A ) ) ) x. ( exp ` ( C x. ( log ` B ) ) ) ) )
58 53 57 eqtrd 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> ( exp ` ( C x. ( log ` ( A x. B ) ) ) ) = ( ( exp ` ( C x. ( log ` A ) ) ) x. ( exp ` ( C x. ( log ` B ) ) ) ) )
59 47 49 mulcld 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> ( A x. B ) e. CC )
60 47 49 36 41 mulne0d 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> ( A x. B ) =/= 0 )
61 cxpef 
 |-  ( ( ( A x. B ) e. CC /\ ( A x. B ) =/= 0 /\ C e. CC ) -> ( ( A x. B ) ^c C ) = ( exp ` ( C x. ( log ` ( A x. B ) ) ) ) )
62 59 60 46 61 syl3anc 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> ( ( A x. B ) ^c C ) = ( exp ` ( C x. ( log ` ( A x. B ) ) ) ) )
63 cxpef 
 |-  ( ( A e. CC /\ A =/= 0 /\ C e. CC ) -> ( A ^c C ) = ( exp ` ( C x. ( log ` A ) ) ) )
64 47 36 46 63 syl3anc 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> ( A ^c C ) = ( exp ` ( C x. ( log ` A ) ) ) )
65 cxpef 
 |-  ( ( B e. CC /\ B =/= 0 /\ C e. CC ) -> ( B ^c C ) = ( exp ` ( C x. ( log ` B ) ) ) )
66 49 41 46 65 syl3anc 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> ( B ^c C ) = ( exp ` ( C x. ( log ` B ) ) ) )
67 64 66 oveq12d 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> ( ( A ^c C ) x. ( B ^c C ) ) = ( ( exp ` ( C x. ( log ` A ) ) ) x. ( exp ` ( C x. ( log ` B ) ) ) ) )
68 58 62 67 3eqtr4d 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> ( ( A x. B ) ^c C ) = ( ( A ^c C ) x. ( B ^c C ) ) )
69 68 exp32 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) -> ( A =/= 0 -> ( B =/= 0 -> ( ( A x. B ) ^c C ) = ( ( A ^c C ) x. ( B ^c C ) ) ) ) )
70 33 69 pm2.61dne 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) -> ( B =/= 0 -> ( ( A x. B ) ^c C ) = ( ( A ^c C ) x. ( B ^c C ) ) ) )
71 13 70 pm2.61dne 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) -> ( ( A x. B ) ^c C ) = ( ( A ^c C ) x. ( B ^c C ) ) )