Step | Hyp | Ref
| Expression |
1 | | elnn0 8290 |
. 2
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℕ
∨ 𝑁 =
0)) |
2 | | simpr 108 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℕ) |
3 | | elnnuz 8655 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈
(ℤ≥‘1)) |
4 | 2, 3 | sylib 120 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
(ℤ≥‘1)) |
5 | | cnex 7097 |
. . . . . . 7
⊢ ℂ
∈ V |
6 | 5 | a1i 9 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ℂ
∈ V) |
7 | | simpll 495 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈
(ℤ≥‘1)) → 𝐴 ∈ ℂ) |
8 | | elnnuz 8655 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℕ ↔ 𝑥 ∈
(ℤ≥‘1)) |
9 | | fvconst2g 5396 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℕ) →
((ℕ × {𝐴})‘𝑥) = 𝐴) |
10 | 9 | eleq1d 2147 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℕ) →
(((ℕ × {𝐴})‘𝑥) ∈ ℂ ↔ 𝐴 ∈ ℂ)) |
11 | 8, 10 | sylan2br 282 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈
(ℤ≥‘1)) → (((ℕ × {𝐴})‘𝑥) ∈ ℂ ↔ 𝐴 ∈ ℂ)) |
12 | 11 | adantlr 460 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈
(ℤ≥‘1)) → (((ℕ × {𝐴})‘𝑥) ∈ ℂ ↔ 𝐴 ∈ ℂ)) |
13 | 7, 12 | mpbird 165 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈
(ℤ≥‘1)) → ((ℕ × {𝐴})‘𝑥) ∈ ℂ) |
14 | | mulcl 7100 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ) |
15 | 14 | adantl 271 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ) |
16 | 4, 6, 13, 15 | iseqp1 9445 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (seq1(
· , (ℕ × {𝐴}), ℂ)‘(𝑁 + 1)) = ((seq1( · , (ℕ ×
{𝐴}), ℂ)‘𝑁) · ((ℕ ×
{𝐴})‘(𝑁 + 1)))) |
17 | | peano2nn 8051 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℕ) |
18 | | fvconst2g 5396 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ (𝑁 + 1) ∈ ℕ) →
((ℕ × {𝐴})‘(𝑁 + 1)) = 𝐴) |
19 | 17, 18 | sylan2 280 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) →
((ℕ × {𝐴})‘(𝑁 + 1)) = 𝐴) |
20 | 19 | oveq2d 5548 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((seq1(
· , (ℕ × {𝐴}), ℂ)‘𝑁) · ((ℕ × {𝐴})‘(𝑁 + 1))) = ((seq1( · , (ℕ
× {𝐴}),
ℂ)‘𝑁) ·
𝐴)) |
21 | 16, 20 | eqtrd 2113 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (seq1(
· , (ℕ × {𝐴}), ℂ)‘(𝑁 + 1)) = ((seq1( · , (ℕ ×
{𝐴}), ℂ)‘𝑁) · 𝐴)) |
22 | | expinnval 9479 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ (𝑁 + 1) ∈ ℕ) →
(𝐴↑(𝑁 + 1)) = (seq1( · , (ℕ ×
{𝐴}), ℂ)‘(𝑁 + 1))) |
23 | 17, 22 | sylan2 280 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (𝐴↑(𝑁 + 1)) = (seq1( · , (ℕ ×
{𝐴}), ℂ)‘(𝑁 + 1))) |
24 | | expinnval 9479 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (𝐴↑𝑁) = (seq1( · , (ℕ ×
{𝐴}), ℂ)‘𝑁)) |
25 | 24 | oveq1d 5547 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((𝐴↑𝑁) · 𝐴) = ((seq1( · , (ℕ ×
{𝐴}), ℂ)‘𝑁) · 𝐴)) |
26 | 21, 23, 25 | 3eqtr4d 2123 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (𝐴↑(𝑁 + 1)) = ((𝐴↑𝑁) · 𝐴)) |
27 | | exp1 9482 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (𝐴↑1) = 𝐴) |
28 | | mulid2 7117 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (1
· 𝐴) = 𝐴) |
29 | 27, 28 | eqtr4d 2116 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (𝐴↑1) = (1 · 𝐴)) |
30 | 29 | adantr 270 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 = 0) → (𝐴↑1) = (1 · 𝐴)) |
31 | | simpr 108 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 = 0) → 𝑁 = 0) |
32 | 31 | oveq1d 5547 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 = 0) → (𝑁 + 1) = (0 + 1)) |
33 | | 0p1e1 8153 |
. . . . . 6
⊢ (0 + 1) =
1 |
34 | 32, 33 | syl6eq 2129 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 = 0) → (𝑁 + 1) = 1) |
35 | 34 | oveq2d 5548 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 = 0) → (𝐴↑(𝑁 + 1)) = (𝐴↑1)) |
36 | | oveq2 5540 |
. . . . . 6
⊢ (𝑁 = 0 → (𝐴↑𝑁) = (𝐴↑0)) |
37 | | exp0 9480 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (𝐴↑0) = 1) |
38 | 36, 37 | sylan9eqr 2135 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 = 0) → (𝐴↑𝑁) = 1) |
39 | 38 | oveq1d 5547 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 = 0) → ((𝐴↑𝑁) · 𝐴) = (1 · 𝐴)) |
40 | 30, 35, 39 | 3eqtr4d 2123 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 = 0) → (𝐴↑(𝑁 + 1)) = ((𝐴↑𝑁) · 𝐴)) |
41 | 26, 40 | jaodan 743 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ (𝑁 ∈ ℕ ∨ 𝑁 = 0)) → (𝐴↑(𝑁 + 1)) = ((𝐴↑𝑁) · 𝐴)) |
42 | 1, 41 | sylan2b 281 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (𝐴↑(𝑁 + 1)) = ((𝐴↑𝑁) · 𝐴)) |