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 ABC0ABC=ABC

Proof

Step Hyp Ref Expression
1 oveq2 x=0Bx=B0
2 1 oveq2d x=0ABx=AB0
3 oveq2 x=0ABx=AB0
4 2 3 eqeq12d x=0ABx=ABxAB0=AB0
5 4 imbi2d x=0ABABx=ABxABAB0=AB0
6 oveq2 x=kBx=Bk
7 6 oveq2d x=kABx=ABk
8 oveq2 x=kABx=ABk
9 7 8 eqeq12d x=kABx=ABxABk=ABk
10 9 imbi2d x=kABABx=ABxABABk=ABk
11 oveq2 x=k+1Bx=Bk+1
12 11 oveq2d x=k+1ABx=ABk+1
13 oveq2 x=k+1ABx=ABk+1
14 12 13 eqeq12d x=k+1ABx=ABxABk+1=ABk+1
15 14 imbi2d x=k+1ABABx=ABxABABk+1=ABk+1
16 oveq2 x=CBx=BC
17 16 oveq2d x=CABx=ABC
18 oveq2 x=CABx=ABC
19 17 18 eqeq12d x=CABx=ABxABC=ABC
20 19 imbi2d x=CABABx=ABxABABC=ABC
21 cxp0 AA0=1
22 21 adantr ABA0=1
23 mul01 BB0=0
24 23 adantl ABB0=0
25 24 oveq2d ABAB0=A0
26 cxpcl ABAB
27 26 exp0d ABAB0=1
28 22 25 27 3eqtr4d ABAB0=AB0
29 oveq1 ABk=ABkABkAB=ABkAB
30 0cn 0
31 cxp0 000=1
32 30 31 ax-mp 00=1
33 1t1e1 11=1
34 32 33 eqtr4i 00=11
35 simplr ABk0A=0B=0A=0
36 simpr ABk0A=0B=0B=0
37 36 oveq1d ABk0A=0B=0Bk+1=0k+1
38 nn0p1nn k0k+1
39 38 adantl ABk0k+1
40 39 nncnd ABk0k+1
41 40 ad2antrr ABk0A=0B=0k+1
42 41 mul02d ABk0A=0B=00k+1=0
43 37 42 eqtrd ABk0A=0B=0Bk+1=0
44 35 43 oveq12d ABk0A=0B=0ABk+1=00
45 36 oveq1d ABk0A=0B=0Bk=0k
46 nn0cn k0k
47 46 adantl ABk0k
48 47 ad2antrr ABk0A=0B=0k
49 48 mul02d ABk0A=0B=00k=0
50 45 49 eqtrd ABk0A=0B=0Bk=0
51 35 50 oveq12d ABk0A=0B=0ABk=00
52 51 32 eqtrdi ABk0A=0B=0ABk=1
53 35 36 oveq12d ABk0A=0B=0AB=00
54 53 32 eqtrdi ABk0A=0B=0AB=1
55 52 54 oveq12d ABk0A=0B=0ABkAB=11
56 34 44 55 3eqtr4a ABk0A=0B=0ABk+1=ABkAB
57 simpll ABk0A
58 57 ad2antrr ABk0A=0B0A
59 simplr ABk0B
60 59 47 mulcld ABk0Bk
61 60 ad2antrr ABk0A=0B0Bk
62 cxpcl ABkABk
63 58 61 62 syl2anc ABk0A=0B0ABk
64 63 mul01d ABk0A=0B0ABk0=0
65 simplr ABk0A=0B0A=0
66 65 oveq1d ABk0A=0B0AB=0B
67 59 ad2antrr ABk0A=0B0B
68 simpr ABk0A=0B0B0
69 0cxp BB00B=0
70 67 68 69 syl2anc ABk0A=0B00B=0
71 66 70 eqtrd ABk0A=0B0AB=0
72 71 oveq2d ABk0A=0B0ABkAB=ABk0
73 65 oveq1d ABk0A=0B0ABk+1=0Bk+1
74 40 ad2antrr ABk0A=0B0k+1
75 67 74 mulcld ABk0A=0B0Bk+1
76 39 nnne0d ABk0k+10
77 76 ad2antrr ABk0A=0B0k+10
78 67 74 68 77 mulne0d ABk0A=0B0Bk+10
79 0cxp Bk+1Bk+100Bk+1=0
80 75 78 79 syl2anc ABk0A=0B00Bk+1=0
81 73 80 eqtrd ABk0A=0B0ABk+1=0
82 64 72 81 3eqtr4rd ABk0A=0B0ABk+1=ABkAB
83 56 82 pm2.61dane ABk0A=0ABk+1=ABkAB
84 59 adantr ABk0A0B
85 47 adantr ABk0A0k
86 1cnd ABk0A01
87 84 85 86 adddid ABk0A0Bk+1=Bk+B1
88 84 mulid1d ABk0A0B1=B
89 88 oveq2d ABk0A0Bk+B1=Bk+B
90 87 89 eqtrd ABk0A0Bk+1=Bk+B
91 90 oveq2d ABk0A0ABk+1=ABk+B
92 57 adantr ABk0A0A
93 simpr ABk0A0A0
94 60 adantr ABk0A0Bk
95 cxpadd AA0BkBABk+B=ABkAB
96 92 93 94 84 95 syl211anc ABk0A0ABk+B=ABkAB
97 91 96 eqtrd ABk0A0ABk+1=ABkAB
98 83 97 pm2.61dane ABk0ABk+1=ABkAB
99 expp1 ABk0ABk+1=ABkAB
100 26 99 sylan ABk0ABk+1=ABkAB
101 98 100 eqeq12d ABk0ABk+1=ABk+1ABkAB=ABkAB
102 29 101 syl5ibr ABk0ABk=ABkABk+1=ABk+1
103 102 expcom k0ABABk=ABkABk+1=ABk+1
104 103 a2d k0ABABk=ABkABABk+1=ABk+1
105 5 10 15 20 28 104 nn0ind C0ABABC=ABC
106 105 com12 ABC0ABC=ABC
107 106 3impia ABC0ABC=ABC