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 an integer. (Contributed by Mario Carneiro, 9-Aug-2014)

Ref Expression
Assertion cxpmul2 A B C 0 A B C = A B C

Proof

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