Step | Hyp | Ref
| Expression |
1 | | oveq2 7221 |
. . . 4
⊢ (𝑗 = 0 → (𝐴↑𝑗) = (𝐴↑0)) |
2 | 1 | fveq2d 6721 |
. . 3
⊢ (𝑗 = 0 →
(∗‘(𝐴↑𝑗)) = (∗‘(𝐴↑0))) |
3 | | oveq2 7221 |
. . 3
⊢ (𝑗 = 0 →
((∗‘𝐴)↑𝑗) = ((∗‘𝐴)↑0)) |
4 | 2, 3 | eqeq12d 2753 |
. 2
⊢ (𝑗 = 0 →
((∗‘(𝐴↑𝑗)) = ((∗‘𝐴)↑𝑗) ↔ (∗‘(𝐴↑0)) = ((∗‘𝐴)↑0))) |
5 | | oveq2 7221 |
. . . 4
⊢ (𝑗 = 𝑘 → (𝐴↑𝑗) = (𝐴↑𝑘)) |
6 | 5 | fveq2d 6721 |
. . 3
⊢ (𝑗 = 𝑘 → (∗‘(𝐴↑𝑗)) = (∗‘(𝐴↑𝑘))) |
7 | | oveq2 7221 |
. . 3
⊢ (𝑗 = 𝑘 → ((∗‘𝐴)↑𝑗) = ((∗‘𝐴)↑𝑘)) |
8 | 6, 7 | eqeq12d 2753 |
. 2
⊢ (𝑗 = 𝑘 → ((∗‘(𝐴↑𝑗)) = ((∗‘𝐴)↑𝑗) ↔ (∗‘(𝐴↑𝑘)) = ((∗‘𝐴)↑𝑘))) |
9 | | oveq2 7221 |
. . . 4
⊢ (𝑗 = (𝑘 + 1) → (𝐴↑𝑗) = (𝐴↑(𝑘 + 1))) |
10 | 9 | fveq2d 6721 |
. . 3
⊢ (𝑗 = (𝑘 + 1) → (∗‘(𝐴↑𝑗)) = (∗‘(𝐴↑(𝑘 + 1)))) |
11 | | oveq2 7221 |
. . 3
⊢ (𝑗 = (𝑘 + 1) → ((∗‘𝐴)↑𝑗) = ((∗‘𝐴)↑(𝑘 + 1))) |
12 | 10, 11 | eqeq12d 2753 |
. 2
⊢ (𝑗 = (𝑘 + 1) → ((∗‘(𝐴↑𝑗)) = ((∗‘𝐴)↑𝑗) ↔ (∗‘(𝐴↑(𝑘 + 1))) = ((∗‘𝐴)↑(𝑘 + 1)))) |
13 | | oveq2 7221 |
. . . 4
⊢ (𝑗 = 𝑁 → (𝐴↑𝑗) = (𝐴↑𝑁)) |
14 | 13 | fveq2d 6721 |
. . 3
⊢ (𝑗 = 𝑁 → (∗‘(𝐴↑𝑗)) = (∗‘(𝐴↑𝑁))) |
15 | | oveq2 7221 |
. . 3
⊢ (𝑗 = 𝑁 → ((∗‘𝐴)↑𝑗) = ((∗‘𝐴)↑𝑁)) |
16 | 14, 15 | eqeq12d 2753 |
. 2
⊢ (𝑗 = 𝑁 → ((∗‘(𝐴↑𝑗)) = ((∗‘𝐴)↑𝑗) ↔ (∗‘(𝐴↑𝑁)) = ((∗‘𝐴)↑𝑁))) |
17 | | exp0 13639 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝐴↑0) = 1) |
18 | 17 | fveq2d 6721 |
. . 3
⊢ (𝐴 ∈ ℂ →
(∗‘(𝐴↑0))
= (∗‘1)) |
19 | | cjcl 14668 |
. . . 4
⊢ (𝐴 ∈ ℂ →
(∗‘𝐴) ∈
ℂ) |
20 | | exp0 13639 |
. . . . 5
⊢
((∗‘𝐴)
∈ ℂ → ((∗‘𝐴)↑0) = 1) |
21 | | 1re 10833 |
. . . . . 6
⊢ 1 ∈
ℝ |
22 | | cjre 14702 |
. . . . . 6
⊢ (1 ∈
ℝ → (∗‘1) = 1) |
23 | 21, 22 | ax-mp 5 |
. . . . 5
⊢
(∗‘1) = 1 |
24 | 20, 23 | eqtr4di 2796 |
. . . 4
⊢
((∗‘𝐴)
∈ ℂ → ((∗‘𝐴)↑0) =
(∗‘1)) |
25 | 19, 24 | syl 17 |
. . 3
⊢ (𝐴 ∈ ℂ →
((∗‘𝐴)↑0)
= (∗‘1)) |
26 | 18, 25 | eqtr4d 2780 |
. 2
⊢ (𝐴 ∈ ℂ →
(∗‘(𝐴↑0))
= ((∗‘𝐴)↑0)) |
27 | | expp1 13642 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴)) |
28 | 27 | fveq2d 6721 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (∗‘(𝐴↑(𝑘 + 1))) = (∗‘((𝐴↑𝑘) · 𝐴))) |
29 | | expcl 13653 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑𝑘) ∈
ℂ) |
30 | | simpl 486 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ 𝐴 ∈
ℂ) |
31 | | cjmul 14705 |
. . . . . 6
⊢ (((𝐴↑𝑘) ∈ ℂ ∧ 𝐴 ∈ ℂ) →
(∗‘((𝐴↑𝑘) · 𝐴)) = ((∗‘(𝐴↑𝑘)) · (∗‘𝐴))) |
32 | 29, 30, 31 | syl2anc 587 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (∗‘((𝐴↑𝑘) · 𝐴)) = ((∗‘(𝐴↑𝑘)) · (∗‘𝐴))) |
33 | 28, 32 | eqtrd 2777 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (∗‘(𝐴↑(𝑘 + 1))) = ((∗‘(𝐴↑𝑘)) · (∗‘𝐴))) |
34 | 33 | adantr 484 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
∧ (∗‘(𝐴↑𝑘)) = ((∗‘𝐴)↑𝑘)) → (∗‘(𝐴↑(𝑘 + 1))) = ((∗‘(𝐴↑𝑘)) · (∗‘𝐴))) |
35 | | oveq1 7220 |
. . . 4
⊢
((∗‘(𝐴↑𝑘)) = ((∗‘𝐴)↑𝑘) → ((∗‘(𝐴↑𝑘)) · (∗‘𝐴)) = (((∗‘𝐴)↑𝑘) · (∗‘𝐴))) |
36 | | expp1 13642 |
. . . . . 6
⊢
(((∗‘𝐴)
∈ ℂ ∧ 𝑘
∈ ℕ0) → ((∗‘𝐴)↑(𝑘 + 1)) = (((∗‘𝐴)↑𝑘) · (∗‘𝐴))) |
37 | 19, 36 | sylan 583 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ ((∗‘𝐴)↑(𝑘 + 1)) = (((∗‘𝐴)↑𝑘) · (∗‘𝐴))) |
38 | 37 | eqcomd 2743 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (((∗‘𝐴)↑𝑘) · (∗‘𝐴)) = ((∗‘𝐴)↑(𝑘 + 1))) |
39 | 35, 38 | sylan9eqr 2800 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
∧ (∗‘(𝐴↑𝑘)) = ((∗‘𝐴)↑𝑘)) → ((∗‘(𝐴↑𝑘)) · (∗‘𝐴)) = ((∗‘𝐴)↑(𝑘 + 1))) |
40 | 34, 39 | eqtrd 2777 |
. 2
⊢ (((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
∧ (∗‘(𝐴↑𝑘)) = ((∗‘𝐴)↑𝑘)) → (∗‘(𝐴↑(𝑘 + 1))) = ((∗‘𝐴)↑(𝑘 + 1))) |
41 | 4, 8, 12, 16, 26, 40 | nn0indd 12274 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (∗‘(𝐴↑𝑁)) = ((∗‘𝐴)↑𝑁)) |