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 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℕ0 ) → ( 𝐴 ↑𝑐 ( 𝐵 · 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) ↑ 𝐶 ) )

Proof

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