Step | Hyp | Ref
| Expression |
1 | | oveq2 5463 |
. . . . . 6
⊢ (𝑗 = 0 → (A↑𝑗) = (A↑0)) |
2 | 1 | fveq2d 5125 |
. . . . 5
⊢ (𝑗 = 0 →
(∗‘(A↑𝑗)) = (∗‘(A↑0))) |
3 | | oveq2 5463 |
. . . . 5
⊢ (𝑗 = 0 →
((∗‘A)↑𝑗) = ((∗‘A)↑0)) |
4 | 2, 3 | eqeq12d 2051 |
. . . 4
⊢ (𝑗 = 0 →
((∗‘(A↑𝑗)) = ((∗‘A)↑𝑗) ↔ (∗‘(A↑0)) = ((∗‘A)↑0))) |
5 | 4 | imbi2d 219 |
. . 3
⊢ (𝑗 = 0 → ((A ∈ ℂ →
(∗‘(A↑𝑗)) = ((∗‘A)↑𝑗)) ↔ (A ∈ ℂ →
(∗‘(A↑0)) =
((∗‘A)↑0)))) |
6 | | oveq2 5463 |
. . . . . 6
⊢ (𝑗 = 𝑘 → (A↑𝑗) = (A↑𝑘)) |
7 | 6 | fveq2d 5125 |
. . . . 5
⊢ (𝑗 = 𝑘 → (∗‘(A↑𝑗)) = (∗‘(A↑𝑘))) |
8 | | oveq2 5463 |
. . . . 5
⊢ (𝑗 = 𝑘 → ((∗‘A)↑𝑗) = ((∗‘A)↑𝑘)) |
9 | 7, 8 | eqeq12d 2051 |
. . . 4
⊢ (𝑗 = 𝑘 → ((∗‘(A↑𝑗)) = ((∗‘A)↑𝑗) ↔ (∗‘(A↑𝑘)) = ((∗‘A)↑𝑘))) |
10 | 9 | imbi2d 219 |
. . 3
⊢ (𝑗 = 𝑘 → ((A ∈ ℂ →
(∗‘(A↑𝑗)) = ((∗‘A)↑𝑗)) ↔ (A ∈ ℂ →
(∗‘(A↑𝑘)) = ((∗‘A)↑𝑘)))) |
11 | | oveq2 5463 |
. . . . . 6
⊢ (𝑗 = (𝑘 + 1) → (A↑𝑗) = (A↑(𝑘 + 1))) |
12 | 11 | fveq2d 5125 |
. . . . 5
⊢ (𝑗 = (𝑘 + 1) → (∗‘(A↑𝑗)) = (∗‘(A↑(𝑘 + 1)))) |
13 | | oveq2 5463 |
. . . . 5
⊢ (𝑗 = (𝑘 + 1) → ((∗‘A)↑𝑗) = ((∗‘A)↑(𝑘 + 1))) |
14 | 12, 13 | eqeq12d 2051 |
. . . 4
⊢ (𝑗 = (𝑘 + 1) → ((∗‘(A↑𝑗)) = ((∗‘A)↑𝑗) ↔ (∗‘(A↑(𝑘 + 1))) = ((∗‘A)↑(𝑘 + 1)))) |
15 | 14 | imbi2d 219 |
. . 3
⊢ (𝑗 = (𝑘 + 1) → ((A ∈ ℂ →
(∗‘(A↑𝑗)) = ((∗‘A)↑𝑗)) ↔ (A ∈ ℂ →
(∗‘(A↑(𝑘 + 1))) = ((∗‘A)↑(𝑘 + 1))))) |
16 | | oveq2 5463 |
. . . . . 6
⊢ (𝑗 = 𝑁 → (A↑𝑗) = (A↑𝑁)) |
17 | 16 | fveq2d 5125 |
. . . . 5
⊢ (𝑗 = 𝑁 → (∗‘(A↑𝑗)) = (∗‘(A↑𝑁))) |
18 | | oveq2 5463 |
. . . . 5
⊢ (𝑗 = 𝑁 → ((∗‘A)↑𝑗) = ((∗‘A)↑𝑁)) |
19 | 17, 18 | eqeq12d 2051 |
. . . 4
⊢ (𝑗 = 𝑁 → ((∗‘(A↑𝑗)) = ((∗‘A)↑𝑗) ↔ (∗‘(A↑𝑁)) = ((∗‘A)↑𝑁))) |
20 | 19 | imbi2d 219 |
. . 3
⊢ (𝑗 = 𝑁 → ((A ∈ ℂ →
(∗‘(A↑𝑗)) = ((∗‘A)↑𝑗)) ↔ (A ∈ ℂ →
(∗‘(A↑𝑁)) = ((∗‘A)↑𝑁)))) |
21 | | exp0 8913 |
. . . . 5
⊢ (A ∈ ℂ →
(A↑0) = 1) |
22 | 21 | fveq2d 5125 |
. . . 4
⊢ (A ∈ ℂ →
(∗‘(A↑0)) =
(∗‘1)) |
23 | | cjcl 9076 |
. . . . 5
⊢ (A ∈ ℂ →
(∗‘A) ∈ ℂ) |
24 | | exp0 8913 |
. . . . . 6
⊢
((∗‘A) ∈ ℂ → ((∗‘A)↑0) = 1) |
25 | | 1re 6824 |
. . . . . . 7
⊢ 1 ∈ ℝ |
26 | | cjre 9110 |
. . . . . . 7
⊢ (1 ∈ ℝ → (∗‘1) =
1) |
27 | 25, 26 | ax-mp 7 |
. . . . . 6
⊢
(∗‘1) = 1 |
28 | 24, 27 | syl6eqr 2087 |
. . . . 5
⊢
((∗‘A) ∈ ℂ → ((∗‘A)↑0) = (∗‘1)) |
29 | 23, 28 | syl 14 |
. . . 4
⊢ (A ∈ ℂ →
((∗‘A)↑0) =
(∗‘1)) |
30 | 22, 29 | eqtr4d 2072 |
. . 3
⊢ (A ∈ ℂ →
(∗‘(A↑0)) =
((∗‘A)↑0)) |
31 | | expp1 8916 |
. . . . . . . . . 10
⊢
((A ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (A↑(𝑘 + 1)) = ((A↑𝑘) · A)) |
32 | 31 | fveq2d 5125 |
. . . . . . . . 9
⊢
((A ∈ ℂ ∧ 𝑘 ∈ ℕ0) →
(∗‘(A↑(𝑘 + 1))) = (∗‘((A↑𝑘) · A))) |
33 | | expcl 8927 |
. . . . . . . . . 10
⊢
((A ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (A↑𝑘) ∈
ℂ) |
34 | | simpl 102 |
. . . . . . . . . 10
⊢
((A ∈ ℂ ∧ 𝑘 ∈ ℕ0) → A ∈
ℂ) |
35 | | cjmul 9113 |
. . . . . . . . . 10
⊢
(((A↑𝑘) ∈ ℂ
∧ A ∈ ℂ) → (∗‘((A↑𝑘) · A)) = ((∗‘(A↑𝑘)) · (∗‘A))) |
36 | 33, 34, 35 | syl2anc 391 |
. . . . . . . . 9
⊢
((A ∈ ℂ ∧ 𝑘 ∈ ℕ0) →
(∗‘((A↑𝑘) · A)) = ((∗‘(A↑𝑘)) · (∗‘A))) |
37 | 32, 36 | eqtrd 2069 |
. . . . . . . 8
⊢
((A ∈ ℂ ∧ 𝑘 ∈ ℕ0) →
(∗‘(A↑(𝑘 + 1))) = ((∗‘(A↑𝑘)) · (∗‘A))) |
38 | 37 | adantr 261 |
. . . . . . 7
⊢
(((A ∈ ℂ ∧ 𝑘 ∈ ℕ0) ∧ (∗‘(A↑𝑘)) = ((∗‘A)↑𝑘)) → (∗‘(A↑(𝑘 + 1))) = ((∗‘(A↑𝑘)) · (∗‘A))) |
39 | | oveq1 5462 |
. . . . . . . 8
⊢
((∗‘(A↑𝑘)) = ((∗‘A)↑𝑘) → ((∗‘(A↑𝑘)) · (∗‘A)) = (((∗‘A)↑𝑘) · (∗‘A))) |
40 | | expp1 8916 |
. . . . . . . . . 10
⊢
(((∗‘A) ∈ ℂ ∧ 𝑘 ∈ ℕ0) →
((∗‘A)↑(𝑘 + 1)) = (((∗‘A)↑𝑘) · (∗‘A))) |
41 | 23, 40 | sylan 267 |
. . . . . . . . 9
⊢
((A ∈ ℂ ∧ 𝑘 ∈ ℕ0) →
((∗‘A)↑(𝑘 + 1)) = (((∗‘A)↑𝑘) · (∗‘A))) |
42 | 41 | eqcomd 2042 |
. . . . . . . 8
⊢
((A ∈ ℂ ∧ 𝑘 ∈ ℕ0) →
(((∗‘A)↑𝑘) · (∗‘A)) = ((∗‘A)↑(𝑘 + 1))) |
43 | 39, 42 | sylan9eqr 2091 |
. . . . . . 7
⊢
(((A ∈ ℂ ∧ 𝑘 ∈ ℕ0) ∧ (∗‘(A↑𝑘)) = ((∗‘A)↑𝑘)) → ((∗‘(A↑𝑘)) · (∗‘A)) = ((∗‘A)↑(𝑘 + 1))) |
44 | 38, 43 | eqtrd 2069 |
. . . . . 6
⊢
(((A ∈ ℂ ∧ 𝑘 ∈ ℕ0) ∧ (∗‘(A↑𝑘)) = ((∗‘A)↑𝑘)) → (∗‘(A↑(𝑘 + 1))) = ((∗‘A)↑(𝑘 + 1))) |
45 | 44 | exp31 346 |
. . . . 5
⊢ (A ∈ ℂ →
(𝑘 ∈ ℕ0 →
((∗‘(A↑𝑘)) = ((∗‘A)↑𝑘) → (∗‘(A↑(𝑘 + 1))) = ((∗‘A)↑(𝑘 + 1))))) |
46 | 45 | com12 27 |
. . . 4
⊢ (𝑘 ∈ ℕ0 → (A ∈ ℂ →
((∗‘(A↑𝑘)) = ((∗‘A)↑𝑘) → (∗‘(A↑(𝑘 + 1))) = ((∗‘A)↑(𝑘 + 1))))) |
47 | 46 | a2d 23 |
. . 3
⊢ (𝑘 ∈ ℕ0 → ((A ∈ ℂ →
(∗‘(A↑𝑘)) = ((∗‘A)↑𝑘)) → (A ∈ ℂ →
(∗‘(A↑(𝑘 + 1))) = ((∗‘A)↑(𝑘 + 1))))) |
48 | 5, 10, 15, 20, 30, 47 | nn0ind 8128 |
. 2
⊢ (𝑁 ∈ ℕ0 → (A ∈ ℂ →
(∗‘(A↑𝑁)) = ((∗‘A)↑𝑁))) |
49 | 48 | impcom 116 |
1
⊢
((A ∈ ℂ ∧ 𝑁 ∈ ℕ0) →
(∗‘(A↑𝑁)) = ((∗‘A)↑𝑁)) |