# 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 eqtrdi $⊢ 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 eqtrdi $⊢ 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$