Step | Hyp | Ref
| Expression |
1 | | oveq2 5861 |
. . . . . 6
⊢ (𝑗 = 0 → (𝐴↑𝑗) = (𝐴↑0)) |
2 | 1 | fveq2d 5500 |
. . . . 5
⊢ (𝑗 = 0 →
(∗‘(𝐴↑𝑗)) = (∗‘(𝐴↑0))) |
3 | | oveq2 5861 |
. . . . 5
⊢ (𝑗 = 0 →
((∗‘𝐴)↑𝑗) = ((∗‘𝐴)↑0)) |
4 | 2, 3 | eqeq12d 2185 |
. . . 4
⊢ (𝑗 = 0 →
((∗‘(𝐴↑𝑗)) = ((∗‘𝐴)↑𝑗) ↔ (∗‘(𝐴↑0)) = ((∗‘𝐴)↑0))) |
5 | 4 | imbi2d 229 |
. . 3
⊢ (𝑗 = 0 → ((𝐴 ∈ ℂ →
(∗‘(𝐴↑𝑗)) = ((∗‘𝐴)↑𝑗)) ↔ (𝐴 ∈ ℂ →
(∗‘(𝐴↑0))
= ((∗‘𝐴)↑0)))) |
6 | | oveq2 5861 |
. . . . . 6
⊢ (𝑗 = 𝑘 → (𝐴↑𝑗) = (𝐴↑𝑘)) |
7 | 6 | fveq2d 5500 |
. . . . 5
⊢ (𝑗 = 𝑘 → (∗‘(𝐴↑𝑗)) = (∗‘(𝐴↑𝑘))) |
8 | | oveq2 5861 |
. . . . 5
⊢ (𝑗 = 𝑘 → ((∗‘𝐴)↑𝑗) = ((∗‘𝐴)↑𝑘)) |
9 | 7, 8 | eqeq12d 2185 |
. . . 4
⊢ (𝑗 = 𝑘 → ((∗‘(𝐴↑𝑗)) = ((∗‘𝐴)↑𝑗) ↔ (∗‘(𝐴↑𝑘)) = ((∗‘𝐴)↑𝑘))) |
10 | 9 | imbi2d 229 |
. . 3
⊢ (𝑗 = 𝑘 → ((𝐴 ∈ ℂ →
(∗‘(𝐴↑𝑗)) = ((∗‘𝐴)↑𝑗)) ↔ (𝐴 ∈ ℂ →
(∗‘(𝐴↑𝑘)) = ((∗‘𝐴)↑𝑘)))) |
11 | | oveq2 5861 |
. . . . . 6
⊢ (𝑗 = (𝑘 + 1) → (𝐴↑𝑗) = (𝐴↑(𝑘 + 1))) |
12 | 11 | fveq2d 5500 |
. . . . 5
⊢ (𝑗 = (𝑘 + 1) → (∗‘(𝐴↑𝑗)) = (∗‘(𝐴↑(𝑘 + 1)))) |
13 | | oveq2 5861 |
. . . . 5
⊢ (𝑗 = (𝑘 + 1) → ((∗‘𝐴)↑𝑗) = ((∗‘𝐴)↑(𝑘 + 1))) |
14 | 12, 13 | eqeq12d 2185 |
. . . 4
⊢ (𝑗 = (𝑘 + 1) → ((∗‘(𝐴↑𝑗)) = ((∗‘𝐴)↑𝑗) ↔ (∗‘(𝐴↑(𝑘 + 1))) = ((∗‘𝐴)↑(𝑘 + 1)))) |
15 | 14 | imbi2d 229 |
. . 3
⊢ (𝑗 = (𝑘 + 1) → ((𝐴 ∈ ℂ →
(∗‘(𝐴↑𝑗)) = ((∗‘𝐴)↑𝑗)) ↔ (𝐴 ∈ ℂ →
(∗‘(𝐴↑(𝑘 + 1))) = ((∗‘𝐴)↑(𝑘 + 1))))) |
16 | | oveq2 5861 |
. . . . . 6
⊢ (𝑗 = 𝑁 → (𝐴↑𝑗) = (𝐴↑𝑁)) |
17 | 16 | fveq2d 5500 |
. . . . 5
⊢ (𝑗 = 𝑁 → (∗‘(𝐴↑𝑗)) = (∗‘(𝐴↑𝑁))) |
18 | | oveq2 5861 |
. . . . 5
⊢ (𝑗 = 𝑁 → ((∗‘𝐴)↑𝑗) = ((∗‘𝐴)↑𝑁)) |
19 | 17, 18 | eqeq12d 2185 |
. . . 4
⊢ (𝑗 = 𝑁 → ((∗‘(𝐴↑𝑗)) = ((∗‘𝐴)↑𝑗) ↔ (∗‘(𝐴↑𝑁)) = ((∗‘𝐴)↑𝑁))) |
20 | 19 | imbi2d 229 |
. . 3
⊢ (𝑗 = 𝑁 → ((𝐴 ∈ ℂ →
(∗‘(𝐴↑𝑗)) = ((∗‘𝐴)↑𝑗)) ↔ (𝐴 ∈ ℂ →
(∗‘(𝐴↑𝑁)) = ((∗‘𝐴)↑𝑁)))) |
21 | | exp0 10480 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (𝐴↑0) = 1) |
22 | 21 | fveq2d 5500 |
. . . 4
⊢ (𝐴 ∈ ℂ →
(∗‘(𝐴↑0))
= (∗‘1)) |
23 | | cjcl 10812 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
(∗‘𝐴) ∈
ℂ) |
24 | | exp0 10480 |
. . . . . 6
⊢
((∗‘𝐴)
∈ ℂ → ((∗‘𝐴)↑0) = 1) |
25 | | 1re 7919 |
. . . . . . 7
⊢ 1 ∈
ℝ |
26 | | cjre 10846 |
. . . . . . 7
⊢ (1 ∈
ℝ → (∗‘1) = 1) |
27 | 25, 26 | ax-mp 5 |
. . . . . 6
⊢
(∗‘1) = 1 |
28 | 24, 27 | eqtr4di 2221 |
. . . . 5
⊢
((∗‘𝐴)
∈ ℂ → ((∗‘𝐴)↑0) =
(∗‘1)) |
29 | 23, 28 | syl 14 |
. . . 4
⊢ (𝐴 ∈ ℂ →
((∗‘𝐴)↑0)
= (∗‘1)) |
30 | 22, 29 | eqtr4d 2206 |
. . 3
⊢ (𝐴 ∈ ℂ →
(∗‘(𝐴↑0))
= ((∗‘𝐴)↑0)) |
31 | | expp1 10483 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴)) |
32 | 31 | fveq2d 5500 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (∗‘(𝐴↑(𝑘 + 1))) = (∗‘((𝐴↑𝑘) · 𝐴))) |
33 | | expcl 10494 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑𝑘) ∈
ℂ) |
34 | | simpl 108 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ 𝐴 ∈
ℂ) |
35 | | cjmul 10849 |
. . . . . . . . . 10
⊢ (((𝐴↑𝑘) ∈ ℂ ∧ 𝐴 ∈ ℂ) →
(∗‘((𝐴↑𝑘) · 𝐴)) = ((∗‘(𝐴↑𝑘)) · (∗‘𝐴))) |
36 | 33, 34, 35 | syl2anc 409 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (∗‘((𝐴↑𝑘) · 𝐴)) = ((∗‘(𝐴↑𝑘)) · (∗‘𝐴))) |
37 | 32, 36 | eqtrd 2203 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (∗‘(𝐴↑(𝑘 + 1))) = ((∗‘(𝐴↑𝑘)) · (∗‘𝐴))) |
38 | 37 | adantr 274 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
∧ (∗‘(𝐴↑𝑘)) = ((∗‘𝐴)↑𝑘)) → (∗‘(𝐴↑(𝑘 + 1))) = ((∗‘(𝐴↑𝑘)) · (∗‘𝐴))) |
39 | | oveq1 5860 |
. . . . . . . 8
⊢
((∗‘(𝐴↑𝑘)) = ((∗‘𝐴)↑𝑘) → ((∗‘(𝐴↑𝑘)) · (∗‘𝐴)) = (((∗‘𝐴)↑𝑘) · (∗‘𝐴))) |
40 | | expp1 10483 |
. . . . . . . . . 10
⊢
(((∗‘𝐴)
∈ ℂ ∧ 𝑘
∈ ℕ0) → ((∗‘𝐴)↑(𝑘 + 1)) = (((∗‘𝐴)↑𝑘) · (∗‘𝐴))) |
41 | 23, 40 | sylan 281 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ ((∗‘𝐴)↑(𝑘 + 1)) = (((∗‘𝐴)↑𝑘) · (∗‘𝐴))) |
42 | 41 | eqcomd 2176 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (((∗‘𝐴)↑𝑘) · (∗‘𝐴)) = ((∗‘𝐴)↑(𝑘 + 1))) |
43 | 39, 42 | sylan9eqr 2225 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
∧ (∗‘(𝐴↑𝑘)) = ((∗‘𝐴)↑𝑘)) → ((∗‘(𝐴↑𝑘)) · (∗‘𝐴)) = ((∗‘𝐴)↑(𝑘 + 1))) |
44 | 38, 43 | eqtrd 2203 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
∧ (∗‘(𝐴↑𝑘)) = ((∗‘𝐴)↑𝑘)) → (∗‘(𝐴↑(𝑘 + 1))) = ((∗‘𝐴)↑(𝑘 + 1))) |
45 | 44 | exp31 362 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (𝑘 ∈ ℕ0
→ ((∗‘(𝐴↑𝑘)) = ((∗‘𝐴)↑𝑘) → (∗‘(𝐴↑(𝑘 + 1))) = ((∗‘𝐴)↑(𝑘 + 1))))) |
46 | 45 | com12 30 |
. . . 4
⊢ (𝑘 ∈ ℕ0
→ (𝐴 ∈ ℂ
→ ((∗‘(𝐴↑𝑘)) = ((∗‘𝐴)↑𝑘) → (∗‘(𝐴↑(𝑘 + 1))) = ((∗‘𝐴)↑(𝑘 + 1))))) |
47 | 46 | a2d 26 |
. . 3
⊢ (𝑘 ∈ ℕ0
→ ((𝐴 ∈ ℂ
→ (∗‘(𝐴↑𝑘)) = ((∗‘𝐴)↑𝑘)) → (𝐴 ∈ ℂ →
(∗‘(𝐴↑(𝑘 + 1))) = ((∗‘𝐴)↑(𝑘 + 1))))) |
48 | 5, 10, 15, 20, 30, 47 | nn0ind 9326 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝐴 ∈ ℂ
→ (∗‘(𝐴↑𝑁)) = ((∗‘𝐴)↑𝑁))) |
49 | 48 | impcom 124 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (∗‘(𝐴↑𝑁)) = ((∗‘𝐴)↑𝑁)) |