Step 
Hyp 
Ref 
Expression 
1 

oveq2 
⊢ ( 𝑗 = 0 → ( 𝐴 ↑ 𝑗 ) = ( 𝐴 ↑ 0 ) ) 
2 
1

fveq2d 
⊢ ( 𝑗 = 0 → ( ∗ ‘ ( 𝐴 ↑ 𝑗 ) ) = ( ∗ ‘ ( 𝐴 ↑ 0 ) ) ) 
3 

oveq2 
⊢ ( 𝑗 = 0 → ( ( ∗ ‘ 𝐴 ) ↑ 𝑗 ) = ( ( ∗ ‘ 𝐴 ) ↑ 0 ) ) 
4 
2 3

eqeq12d 
⊢ ( 𝑗 = 0 → ( ( ∗ ‘ ( 𝐴 ↑ 𝑗 ) ) = ( ( ∗ ‘ 𝐴 ) ↑ 𝑗 ) ↔ ( ∗ ‘ ( 𝐴 ↑ 0 ) ) = ( ( ∗ ‘ 𝐴 ) ↑ 0 ) ) ) 
5 

oveq2 
⊢ ( 𝑗 = 𝑘 → ( 𝐴 ↑ 𝑗 ) = ( 𝐴 ↑ 𝑘 ) ) 
6 
5

fveq2d 
⊢ ( 𝑗 = 𝑘 → ( ∗ ‘ ( 𝐴 ↑ 𝑗 ) ) = ( ∗ ‘ ( 𝐴 ↑ 𝑘 ) ) ) 
7 

oveq2 
⊢ ( 𝑗 = 𝑘 → ( ( ∗ ‘ 𝐴 ) ↑ 𝑗 ) = ( ( ∗ ‘ 𝐴 ) ↑ 𝑘 ) ) 
8 
6 7

eqeq12d 
⊢ ( 𝑗 = 𝑘 → ( ( ∗ ‘ ( 𝐴 ↑ 𝑗 ) ) = ( ( ∗ ‘ 𝐴 ) ↑ 𝑗 ) ↔ ( ∗ ‘ ( 𝐴 ↑ 𝑘 ) ) = ( ( ∗ ‘ 𝐴 ) ↑ 𝑘 ) ) ) 
9 

oveq2 
⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝐴 ↑ 𝑗 ) = ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) 
10 
9

fveq2d 
⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ∗ ‘ ( 𝐴 ↑ 𝑗 ) ) = ( ∗ ‘ ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) ) 
11 

oveq2 
⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( ∗ ‘ 𝐴 ) ↑ 𝑗 ) = ( ( ∗ ‘ 𝐴 ) ↑ ( 𝑘 + 1 ) ) ) 
12 
10 11

eqeq12d 
⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( ∗ ‘ ( 𝐴 ↑ 𝑗 ) ) = ( ( ∗ ‘ 𝐴 ) ↑ 𝑗 ) ↔ ( ∗ ‘ ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) = ( ( ∗ ‘ 𝐴 ) ↑ ( 𝑘 + 1 ) ) ) ) 
13 

oveq2 
⊢ ( 𝑗 = 𝑁 → ( 𝐴 ↑ 𝑗 ) = ( 𝐴 ↑ 𝑁 ) ) 
14 
13

fveq2d 
⊢ ( 𝑗 = 𝑁 → ( ∗ ‘ ( 𝐴 ↑ 𝑗 ) ) = ( ∗ ‘ ( 𝐴 ↑ 𝑁 ) ) ) 
15 

oveq2 
⊢ ( 𝑗 = 𝑁 → ( ( ∗ ‘ 𝐴 ) ↑ 𝑗 ) = ( ( ∗ ‘ 𝐴 ) ↑ 𝑁 ) ) 
16 
14 15

eqeq12d 
⊢ ( 𝑗 = 𝑁 → ( ( ∗ ‘ ( 𝐴 ↑ 𝑗 ) ) = ( ( ∗ ‘ 𝐴 ) ↑ 𝑗 ) ↔ ( ∗ ‘ ( 𝐴 ↑ 𝑁 ) ) = ( ( ∗ ‘ 𝐴 ) ↑ 𝑁 ) ) ) 
17 

exp0 
⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 0 ) = 1 ) 
18 
17

fveq2d 
⊢ ( 𝐴 ∈ ℂ → ( ∗ ‘ ( 𝐴 ↑ 0 ) ) = ( ∗ ‘ 1 ) ) 
19 

cjcl 
⊢ ( 𝐴 ∈ ℂ → ( ∗ ‘ 𝐴 ) ∈ ℂ ) 
20 

exp0 
⊢ ( ( ∗ ‘ 𝐴 ) ∈ ℂ → ( ( ∗ ‘ 𝐴 ) ↑ 0 ) = 1 ) 
21 

1re 
⊢ 1 ∈ ℝ 
22 

cjre 
⊢ ( 1 ∈ ℝ → ( ∗ ‘ 1 ) = 1 ) 
23 
21 22

axmp 
⊢ ( ∗ ‘ 1 ) = 1 
24 
20 23

eqtr4di 
⊢ ( ( ∗ ‘ 𝐴 ) ∈ ℂ → ( ( ∗ ‘ 𝐴 ) ↑ 0 ) = ( ∗ ‘ 1 ) ) 
25 
19 24

syl 
⊢ ( 𝐴 ∈ ℂ → ( ( ∗ ‘ 𝐴 ) ↑ 0 ) = ( ∗ ‘ 1 ) ) 
26 
18 25

eqtr4d 
⊢ ( 𝐴 ∈ ℂ → ( ∗ ‘ ( 𝐴 ↑ 0 ) ) = ( ( ∗ ‘ 𝐴 ) ↑ 0 ) ) 
27 

expp1 
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ_{0} ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) = ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) ) 
28 
27

fveq2d 
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ_{0} ) → ( ∗ ‘ ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) = ( ∗ ‘ ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) ) ) 
29 

expcl 
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ_{0} ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ ) 
30 

simpl 
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ_{0} ) → 𝐴 ∈ ℂ ) 
31 

cjmul 
⊢ ( ( ( 𝐴 ↑ 𝑘 ) ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ∗ ‘ ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) ) = ( ( ∗ ‘ ( 𝐴 ↑ 𝑘 ) ) · ( ∗ ‘ 𝐴 ) ) ) 
32 
29 30 31

syl2anc 
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ_{0} ) → ( ∗ ‘ ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) ) = ( ( ∗ ‘ ( 𝐴 ↑ 𝑘 ) ) · ( ∗ ‘ 𝐴 ) ) ) 
33 
28 32

eqtrd 
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ_{0} ) → ( ∗ ‘ ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) = ( ( ∗ ‘ ( 𝐴 ↑ 𝑘 ) ) · ( ∗ ‘ 𝐴 ) ) ) 
34 
33

adantr 
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ_{0} ) ∧ ( ∗ ‘ ( 𝐴 ↑ 𝑘 ) ) = ( ( ∗ ‘ 𝐴 ) ↑ 𝑘 ) ) → ( ∗ ‘ ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) = ( ( ∗ ‘ ( 𝐴 ↑ 𝑘 ) ) · ( ∗ ‘ 𝐴 ) ) ) 
35 

oveq1 
⊢ ( ( ∗ ‘ ( 𝐴 ↑ 𝑘 ) ) = ( ( ∗ ‘ 𝐴 ) ↑ 𝑘 ) → ( ( ∗ ‘ ( 𝐴 ↑ 𝑘 ) ) · ( ∗ ‘ 𝐴 ) ) = ( ( ( ∗ ‘ 𝐴 ) ↑ 𝑘 ) · ( ∗ ‘ 𝐴 ) ) ) 
36 

expp1 
⊢ ( ( ( ∗ ‘ 𝐴 ) ∈ ℂ ∧ 𝑘 ∈ ℕ_{0} ) → ( ( ∗ ‘ 𝐴 ) ↑ ( 𝑘 + 1 ) ) = ( ( ( ∗ ‘ 𝐴 ) ↑ 𝑘 ) · ( ∗ ‘ 𝐴 ) ) ) 
37 
19 36

sylan 
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ_{0} ) → ( ( ∗ ‘ 𝐴 ) ↑ ( 𝑘 + 1 ) ) = ( ( ( ∗ ‘ 𝐴 ) ↑ 𝑘 ) · ( ∗ ‘ 𝐴 ) ) ) 
38 
37

eqcomd 
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ_{0} ) → ( ( ( ∗ ‘ 𝐴 ) ↑ 𝑘 ) · ( ∗ ‘ 𝐴 ) ) = ( ( ∗ ‘ 𝐴 ) ↑ ( 𝑘 + 1 ) ) ) 
39 
35 38

sylan9eqr 
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ_{0} ) ∧ ( ∗ ‘ ( 𝐴 ↑ 𝑘 ) ) = ( ( ∗ ‘ 𝐴 ) ↑ 𝑘 ) ) → ( ( ∗ ‘ ( 𝐴 ↑ 𝑘 ) ) · ( ∗ ‘ 𝐴 ) ) = ( ( ∗ ‘ 𝐴 ) ↑ ( 𝑘 + 1 ) ) ) 
40 
34 39

eqtrd 
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ_{0} ) ∧ ( ∗ ‘ ( 𝐴 ↑ 𝑘 ) ) = ( ( ∗ ‘ 𝐴 ) ↑ 𝑘 ) ) → ( ∗ ‘ ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) = ( ( ∗ ‘ 𝐴 ) ↑ ( 𝑘 + 1 ) ) ) 
41 
4 8 12 16 26 40

nn0indd 
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ_{0} ) → ( ∗ ‘ ( 𝐴 ↑ 𝑁 ) ) = ( ( ∗ ‘ 𝐴 ) ↑ 𝑁 ) ) 