Metamath Proof Explorer

Theorem cxpmul2

Description: Product of exponents law for complex exponentiation. Variation on cxpmul with more general conditions on A and B when C is a nonnegative integer. (Contributed by Mario Carneiro, 9-Aug-2014)

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

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( x = 0 -> ( B x. x ) = ( B x. 0 ) )
2 1 oveq2d 
 |-  ( x = 0 -> ( A ^c ( B x. x ) ) = ( A ^c ( B x. 0 ) ) )
3 oveq2 
 |-  ( x = 0 -> ( ( A ^c B ) ^ x ) = ( ( A ^c B ) ^ 0 ) )
4 2 3 eqeq12d 
 |-  ( x = 0 -> ( ( A ^c ( B x. x ) ) = ( ( A ^c B ) ^ x ) <-> ( A ^c ( B x. 0 ) ) = ( ( A ^c B ) ^ 0 ) ) )
5 4 imbi2d 
 |-  ( x = 0 -> ( ( ( A e. CC /\ B e. CC ) -> ( A ^c ( B x. x ) ) = ( ( A ^c B ) ^ x ) ) <-> ( ( A e. CC /\ B e. CC ) -> ( A ^c ( B x. 0 ) ) = ( ( A ^c B ) ^ 0 ) ) ) )
6 oveq2 
 |-  ( x = k -> ( B x. x ) = ( B x. k ) )
7 6 oveq2d 
 |-  ( x = k -> ( A ^c ( B x. x ) ) = ( A ^c ( B x. k ) ) )
8 oveq2 
 |-  ( x = k -> ( ( A ^c B ) ^ x ) = ( ( A ^c B ) ^ k ) )
9 7 8 eqeq12d 
 |-  ( x = k -> ( ( A ^c ( B x. x ) ) = ( ( A ^c B ) ^ x ) <-> ( A ^c ( B x. k ) ) = ( ( A ^c B ) ^ k ) ) )
10 9 imbi2d 
 |-  ( x = k -> ( ( ( A e. CC /\ B e. CC ) -> ( A ^c ( B x. x ) ) = ( ( A ^c B ) ^ x ) ) <-> ( ( A e. CC /\ B e. CC ) -> ( A ^c ( B x. k ) ) = ( ( A ^c B ) ^ k ) ) ) )
11 oveq2 
 |-  ( x = ( k + 1 ) -> ( B x. x ) = ( B x. ( k + 1 ) ) )
12 11 oveq2d 
 |-  ( x = ( k + 1 ) -> ( A ^c ( B x. x ) ) = ( A ^c ( B x. ( k + 1 ) ) ) )
13 oveq2 
 |-  ( x = ( k + 1 ) -> ( ( A ^c B ) ^ x ) = ( ( A ^c B ) ^ ( k + 1 ) ) )
14 12 13 eqeq12d 
 |-  ( x = ( k + 1 ) -> ( ( A ^c ( B x. x ) ) = ( ( A ^c B ) ^ x ) <-> ( A ^c ( B x. ( k + 1 ) ) ) = ( ( A ^c B ) ^ ( k + 1 ) ) ) )
15 14 imbi2d 
 |-  ( x = ( k + 1 ) -> ( ( ( A e. CC /\ B e. CC ) -> ( A ^c ( B x. x ) ) = ( ( A ^c B ) ^ x ) ) <-> ( ( A e. CC /\ B e. CC ) -> ( A ^c ( B x. ( k + 1 ) ) ) = ( ( A ^c B ) ^ ( k + 1 ) ) ) ) )
16 oveq2 
 |-  ( x = C -> ( B x. x ) = ( B x. C ) )
17 16 oveq2d 
 |-  ( x = C -> ( A ^c ( B x. x ) ) = ( A ^c ( B x. C ) ) )
18 oveq2 
 |-  ( x = C -> ( ( A ^c B ) ^ x ) = ( ( A ^c B ) ^ C ) )
19 17 18 eqeq12d 
 |-  ( x = C -> ( ( A ^c ( B x. x ) ) = ( ( A ^c B ) ^ x ) <-> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^ C ) ) )
20 19 imbi2d 
 |-  ( x = C -> ( ( ( A e. CC /\ B e. CC ) -> ( A ^c ( B x. x ) ) = ( ( A ^c B ) ^ x ) ) <-> ( ( A e. CC /\ B e. CC ) -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^ C ) ) ) )
21 cxp0 
 |-  ( A e. CC -> ( A ^c 0 ) = 1 )
22 21 adantr 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A ^c 0 ) = 1 )
23 mul01 
 |-  ( B e. CC -> ( B x. 0 ) = 0 )
24 23 adantl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( B x. 0 ) = 0 )
25 24 oveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A ^c ( B x. 0 ) ) = ( A ^c 0 ) )
26 cxpcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A ^c B ) e. CC )
27 26 exp0d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A ^c B ) ^ 0 ) = 1 )
28 22 25 27 3eqtr4d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A ^c ( B x. 0 ) ) = ( ( A ^c B ) ^ 0 ) )
29 oveq1 
 |-  ( ( A ^c ( B x. k ) ) = ( ( A ^c B ) ^ k ) -> ( ( A ^c ( B x. k ) ) x. ( A ^c B ) ) = ( ( ( A ^c B ) ^ k ) x. ( A ^c B ) ) )
30 0cn 
 |-  0 e. CC
31 cxp0 
 |-  ( 0 e. CC -> ( 0 ^c 0 ) = 1 )
32 30 31 ax-mp 
 |-  ( 0 ^c 0 ) = 1
33 1t1e1 
 |-  ( 1 x. 1 ) = 1
34 32 33 eqtr4i 
 |-  ( 0 ^c 0 ) = ( 1 x. 1 )
35 simplr 
 |-  ( ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) /\ B = 0 ) -> A = 0 )
36 simpr 
 |-  ( ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) /\ B = 0 ) -> B = 0 )
37 36 oveq1d 
 |-  ( ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) /\ B = 0 ) -> ( B x. ( k + 1 ) ) = ( 0 x. ( k + 1 ) ) )
38 nn0p1nn 
 |-  ( k e. NN0 -> ( k + 1 ) e. NN )
39 38 adantl 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) -> ( k + 1 ) e. NN )
40 39 nncnd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) -> ( k + 1 ) e. CC )
41 40 ad2antrr 
 |-  ( ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) /\ B = 0 ) -> ( k + 1 ) e. CC )
42 41 mul02d 
 |-  ( ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) /\ B = 0 ) -> ( 0 x. ( k + 1 ) ) = 0 )
43 37 42 eqtrd 
 |-  ( ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) /\ B = 0 ) -> ( B x. ( k + 1 ) ) = 0 )
44 35 43 oveq12d 
 |-  ( ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) /\ B = 0 ) -> ( A ^c ( B x. ( k + 1 ) ) ) = ( 0 ^c 0 ) )
45 36 oveq1d 
 |-  ( ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) /\ B = 0 ) -> ( B x. k ) = ( 0 x. k ) )
46 nn0cn 
 |-  ( k e. NN0 -> k e. CC )
47 46 adantl 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) -> k e. CC )
48 47 ad2antrr 
 |-  ( ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) /\ B = 0 ) -> k e. CC )
49 48 mul02d 
 |-  ( ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) /\ B = 0 ) -> ( 0 x. k ) = 0 )
50 45 49 eqtrd 
 |-  ( ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) /\ B = 0 ) -> ( B x. k ) = 0 )
51 35 50 oveq12d 
 |-  ( ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) /\ B = 0 ) -> ( A ^c ( B x. k ) ) = ( 0 ^c 0 ) )
52 51 32 eqtrdi 
 |-  ( ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) /\ B = 0 ) -> ( A ^c ( B x. k ) ) = 1 )
53 35 36 oveq12d 
 |-  ( ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) /\ B = 0 ) -> ( A ^c B ) = ( 0 ^c 0 ) )
54 53 32 eqtrdi 
 |-  ( ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) /\ B = 0 ) -> ( A ^c B ) = 1 )
55 52 54 oveq12d 
 |-  ( ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) /\ B = 0 ) -> ( ( A ^c ( B x. k ) ) x. ( A ^c B ) ) = ( 1 x. 1 ) )
56 34 44 55 3eqtr4a 
 |-  ( ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) /\ B = 0 ) -> ( A ^c ( B x. ( k + 1 ) ) ) = ( ( A ^c ( B x. k ) ) x. ( A ^c B ) ) )
57 simpll 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) -> A e. CC )
58 57 ad2antrr 
 |-  ( ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) /\ B =/= 0 ) -> A e. CC )
59 simplr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) -> B e. CC )
60 59 47 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) -> ( B x. k ) e. CC )
61 60 ad2antrr 
 |-  ( ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) /\ B =/= 0 ) -> ( B x. k ) e. CC )
62 cxpcl 
 |-  ( ( A e. CC /\ ( B x. k ) e. CC ) -> ( A ^c ( B x. k ) ) e. CC )
63 58 61 62 syl2anc 
 |-  ( ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) /\ B =/= 0 ) -> ( A ^c ( B x. k ) ) e. CC )
64 63 mul01d 
 |-  ( ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) /\ B =/= 0 ) -> ( ( A ^c ( B x. k ) ) x. 0 ) = 0 )
65 simplr 
 |-  ( ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) /\ B =/= 0 ) -> A = 0 )
66 65 oveq1d 
 |-  ( ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) /\ B =/= 0 ) -> ( A ^c B ) = ( 0 ^c B ) )
67 59 ad2antrr 
 |-  ( ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) /\ B =/= 0 ) -> B e. CC )
68 simpr 
 |-  ( ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) /\ B =/= 0 ) -> B =/= 0 )
69 0cxp 
 |-  ( ( B e. CC /\ B =/= 0 ) -> ( 0 ^c B ) = 0 )
70 67 68 69 syl2anc 
 |-  ( ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) /\ B =/= 0 ) -> ( 0 ^c B ) = 0 )
71 66 70 eqtrd 
 |-  ( ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) /\ B =/= 0 ) -> ( A ^c B ) = 0 )
72 71 oveq2d 
 |-  ( ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) /\ B =/= 0 ) -> ( ( A ^c ( B x. k ) ) x. ( A ^c B ) ) = ( ( A ^c ( B x. k ) ) x. 0 ) )
73 65 oveq1d 
 |-  ( ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) /\ B =/= 0 ) -> ( A ^c ( B x. ( k + 1 ) ) ) = ( 0 ^c ( B x. ( k + 1 ) ) ) )
74 40 ad2antrr 
 |-  ( ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) /\ B =/= 0 ) -> ( k + 1 ) e. CC )
75 67 74 mulcld 
 |-  ( ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) /\ B =/= 0 ) -> ( B x. ( k + 1 ) ) e. CC )
76 39 nnne0d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) -> ( k + 1 ) =/= 0 )
77 76 ad2antrr 
 |-  ( ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) /\ B =/= 0 ) -> ( k + 1 ) =/= 0 )
78 67 74 68 77 mulne0d 
 |-  ( ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) /\ B =/= 0 ) -> ( B x. ( k + 1 ) ) =/= 0 )
79 0cxp 
 |-  ( ( ( B x. ( k + 1 ) ) e. CC /\ ( B x. ( k + 1 ) ) =/= 0 ) -> ( 0 ^c ( B x. ( k + 1 ) ) ) = 0 )
80 75 78 79 syl2anc 
 |-  ( ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) /\ B =/= 0 ) -> ( 0 ^c ( B x. ( k + 1 ) ) ) = 0 )
81 73 80 eqtrd 
 |-  ( ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) /\ B =/= 0 ) -> ( A ^c ( B x. ( k + 1 ) ) ) = 0 )
82 64 72 81 3eqtr4rd 
 |-  ( ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) /\ B =/= 0 ) -> ( A ^c ( B x. ( k + 1 ) ) ) = ( ( A ^c ( B x. k ) ) x. ( A ^c B ) ) )
83 56 82 pm2.61dane 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A = 0 ) -> ( A ^c ( B x. ( k + 1 ) ) ) = ( ( A ^c ( B x. k ) ) x. ( A ^c B ) ) )
84 59 adantr 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A =/= 0 ) -> B e. CC )
85 47 adantr 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A =/= 0 ) -> k e. CC )
86 1cnd 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A =/= 0 ) -> 1 e. CC )
87 84 85 86 adddid 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A =/= 0 ) -> ( B x. ( k + 1 ) ) = ( ( B x. k ) + ( B x. 1 ) ) )
88 84 mulridd 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A =/= 0 ) -> ( B x. 1 ) = B )
89 88 oveq2d 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A =/= 0 ) -> ( ( B x. k ) + ( B x. 1 ) ) = ( ( B x. k ) + B ) )
90 87 89 eqtrd 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A =/= 0 ) -> ( B x. ( k + 1 ) ) = ( ( B x. k ) + B ) )
91 90 oveq2d 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A =/= 0 ) -> ( A ^c ( B x. ( k + 1 ) ) ) = ( A ^c ( ( B x. k ) + B ) ) )
92 57 adantr 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A =/= 0 ) -> A e. CC )
93 simpr 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A =/= 0 ) -> A =/= 0 )
94 60 adantr 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A =/= 0 ) -> ( B x. k ) e. CC )
95 cxpadd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B x. k ) e. CC /\ B e. CC ) -> ( A ^c ( ( B x. k ) + B ) ) = ( ( A ^c ( B x. k ) ) x. ( A ^c B ) ) )
96 92 93 94 84 95 syl211anc 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A =/= 0 ) -> ( A ^c ( ( B x. k ) + B ) ) = ( ( A ^c ( B x. k ) ) x. ( A ^c B ) ) )
97 91 96 eqtrd 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ A =/= 0 ) -> ( A ^c ( B x. ( k + 1 ) ) ) = ( ( A ^c ( B x. k ) ) x. ( A ^c B ) ) )
98 83 97 pm2.61dane 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) -> ( A ^c ( B x. ( k + 1 ) ) ) = ( ( A ^c ( B x. k ) ) x. ( A ^c B ) ) )
99 expp1 
 |-  ( ( ( A ^c B ) e. CC /\ k e. NN0 ) -> ( ( A ^c B ) ^ ( k + 1 ) ) = ( ( ( A ^c B ) ^ k ) x. ( A ^c B ) ) )
100 26 99 sylan 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) -> ( ( A ^c B ) ^ ( k + 1 ) ) = ( ( ( A ^c B ) ^ k ) x. ( A ^c B ) ) )
101 98 100 eqeq12d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) -> ( ( A ^c ( B x. ( k + 1 ) ) ) = ( ( A ^c B ) ^ ( k + 1 ) ) <-> ( ( A ^c ( B x. k ) ) x. ( A ^c B ) ) = ( ( ( A ^c B ) ^ k ) x. ( A ^c B ) ) ) )
102 29 101 imbitrrid 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) -> ( ( A ^c ( B x. k ) ) = ( ( A ^c B ) ^ k ) -> ( A ^c ( B x. ( k + 1 ) ) ) = ( ( A ^c B ) ^ ( k + 1 ) ) ) )
103 102 expcom 
 |-  ( k e. NN0 -> ( ( A e. CC /\ B e. CC ) -> ( ( A ^c ( B x. k ) ) = ( ( A ^c B ) ^ k ) -> ( A ^c ( B x. ( k + 1 ) ) ) = ( ( A ^c B ) ^ ( k + 1 ) ) ) ) )
104 103 a2d 
 |-  ( k e. NN0 -> ( ( ( A e. CC /\ B e. CC ) -> ( A ^c ( B x. k ) ) = ( ( A ^c B ) ^ k ) ) -> ( ( A e. CC /\ B e. CC ) -> ( A ^c ( B x. ( k + 1 ) ) ) = ( ( A ^c B ) ^ ( k + 1 ) ) ) ) )
105 5 10 15 20 28 104 nn0ind 
 |-  ( C e. NN0 -> ( ( A e. CC /\ B e. CC ) -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^ C ) ) )
106 105 com12 
 |-  ( ( A e. CC /\ B e. CC ) -> ( C e. NN0 -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^ C ) ) )
107 106 3impia 
 |-  ( ( A e. CC /\ B e. CC /\ C e. NN0 ) -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^ C ) )