| Step | Hyp | Ref
| Expression |
| 1 | | 0cn 11253 |
. . 3
⊢ 0 ∈
ℂ |
| 2 | | coefv0.1 |
. . . 4
⊢ 𝐴 = (coeff‘𝐹) |
| 3 | | eqid 2737 |
. . . 4
⊢
(deg‘𝐹) =
(deg‘𝐹) |
| 4 | 2, 3 | coeid2 26278 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 0 ∈ ℂ) →
(𝐹‘0) = Σ𝑘 ∈ (0...(deg‘𝐹))((𝐴‘𝑘) · (0↑𝑘))) |
| 5 | 1, 4 | mpan2 691 |
. 2
⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹‘0) = Σ𝑘 ∈ (0...(deg‘𝐹))((𝐴‘𝑘) · (0↑𝑘))) |
| 6 | | dgrcl 26272 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) ∈
ℕ0) |
| 7 | | nn0uz 12920 |
. . . . 5
⊢
ℕ0 = (ℤ≥‘0) |
| 8 | 6, 7 | eleqtrdi 2851 |
. . . 4
⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) ∈
(ℤ≥‘0)) |
| 9 | | fzss2 13604 |
. . . 4
⊢
((deg‘𝐹)
∈ (ℤ≥‘0) → (0...0) ⊆
(0...(deg‘𝐹))) |
| 10 | 8, 9 | syl 17 |
. . 3
⊢ (𝐹 ∈ (Poly‘𝑆) → (0...0) ⊆
(0...(deg‘𝐹))) |
| 11 | | elfz1eq 13575 |
. . . . . 6
⊢ (𝑘 ∈ (0...0) → 𝑘 = 0) |
| 12 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑘 = 0 → (𝐴‘𝑘) = (𝐴‘0)) |
| 13 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑘 = 0 → (0↑𝑘) = (0↑0)) |
| 14 | | 0exp0e1 14107 |
. . . . . . . 8
⊢
(0↑0) = 1 |
| 15 | 13, 14 | eqtrdi 2793 |
. . . . . . 7
⊢ (𝑘 = 0 → (0↑𝑘) = 1) |
| 16 | 12, 15 | oveq12d 7449 |
. . . . . 6
⊢ (𝑘 = 0 → ((𝐴‘𝑘) · (0↑𝑘)) = ((𝐴‘0) · 1)) |
| 17 | 11, 16 | syl 17 |
. . . . 5
⊢ (𝑘 ∈ (0...0) → ((𝐴‘𝑘) · (0↑𝑘)) = ((𝐴‘0) · 1)) |
| 18 | 2 | coef3 26271 |
. . . . . . 7
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶ℂ) |
| 19 | | 0nn0 12541 |
. . . . . . 7
⊢ 0 ∈
ℕ0 |
| 20 | | ffvelcdm 7101 |
. . . . . . 7
⊢ ((𝐴:ℕ0⟶ℂ ∧ 0
∈ ℕ0) → (𝐴‘0) ∈ ℂ) |
| 21 | 18, 19, 20 | sylancl 586 |
. . . . . 6
⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐴‘0) ∈ ℂ) |
| 22 | 21 | mulridd 11278 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘𝑆) → ((𝐴‘0) · 1) = (𝐴‘0)) |
| 23 | 17, 22 | sylan9eqr 2799 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑘 ∈ (0...0)) → ((𝐴‘𝑘) · (0↑𝑘)) = (𝐴‘0)) |
| 24 | 21 | adantr 480 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑘 ∈ (0...0)) → (𝐴‘0) ∈ ℂ) |
| 25 | 23, 24 | eqeltrd 2841 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑘 ∈ (0...0)) → ((𝐴‘𝑘) · (0↑𝑘)) ∈ ℂ) |
| 26 | | eldifn 4132 |
. . . . . . . 8
⊢ (𝑘 ∈ ((0...(deg‘𝐹)) ∖ (0...0)) → ¬
𝑘 ∈
(0...0)) |
| 27 | | eldifi 4131 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ((0...(deg‘𝐹)) ∖ (0...0)) → 𝑘 ∈ (0...(deg‘𝐹))) |
| 28 | | elfznn0 13660 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (0...(deg‘𝐹)) → 𝑘 ∈ ℕ0) |
| 29 | 27, 28 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ((0...(deg‘𝐹)) ∖ (0...0)) → 𝑘 ∈
ℕ0) |
| 30 | | elnn0 12528 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
↔ (𝑘 ∈ ℕ
∨ 𝑘 =
0)) |
| 31 | 29, 30 | sylib 218 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((0...(deg‘𝐹)) ∖ (0...0)) →
(𝑘 ∈ ℕ ∨
𝑘 = 0)) |
| 32 | 31 | ord 865 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((0...(deg‘𝐹)) ∖ (0...0)) →
(¬ 𝑘 ∈ ℕ
→ 𝑘 =
0)) |
| 33 | | id 22 |
. . . . . . . . . 10
⊢ (𝑘 = 0 → 𝑘 = 0) |
| 34 | | 0z 12624 |
. . . . . . . . . . 11
⊢ 0 ∈
ℤ |
| 35 | | elfz3 13574 |
. . . . . . . . . . 11
⊢ (0 ∈
ℤ → 0 ∈ (0...0)) |
| 36 | 34, 35 | ax-mp 5 |
. . . . . . . . . 10
⊢ 0 ∈
(0...0) |
| 37 | 33, 36 | eqeltrdi 2849 |
. . . . . . . . 9
⊢ (𝑘 = 0 → 𝑘 ∈ (0...0)) |
| 38 | 32, 37 | syl6 35 |
. . . . . . . 8
⊢ (𝑘 ∈ ((0...(deg‘𝐹)) ∖ (0...0)) →
(¬ 𝑘 ∈ ℕ
→ 𝑘 ∈
(0...0))) |
| 39 | 26, 38 | mt3d 148 |
. . . . . . 7
⊢ (𝑘 ∈ ((0...(deg‘𝐹)) ∖ (0...0)) → 𝑘 ∈
ℕ) |
| 40 | 39 | adantl 481 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑘 ∈ ((0...(deg‘𝐹)) ∖ (0...0))) → 𝑘 ∈
ℕ) |
| 41 | 40 | 0expd 14179 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑘 ∈ ((0...(deg‘𝐹)) ∖ (0...0))) → (0↑𝑘) = 0) |
| 42 | 41 | oveq2d 7447 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑘 ∈ ((0...(deg‘𝐹)) ∖ (0...0))) → ((𝐴‘𝑘) · (0↑𝑘)) = ((𝐴‘𝑘) · 0)) |
| 43 | | ffvelcdm 7101 |
. . . . . 6
⊢ ((𝐴:ℕ0⟶ℂ ∧
𝑘 ∈
ℕ0) → (𝐴‘𝑘) ∈ ℂ) |
| 44 | 18, 29, 43 | syl2an 596 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑘 ∈ ((0...(deg‘𝐹)) ∖ (0...0))) → (𝐴‘𝑘) ∈ ℂ) |
| 45 | 44 | mul01d 11460 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑘 ∈ ((0...(deg‘𝐹)) ∖ (0...0))) → ((𝐴‘𝑘) · 0) = 0) |
| 46 | 42, 45 | eqtrd 2777 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑘 ∈ ((0...(deg‘𝐹)) ∖ (0...0))) → ((𝐴‘𝑘) · (0↑𝑘)) = 0) |
| 47 | | fzfid 14014 |
. . 3
⊢ (𝐹 ∈ (Poly‘𝑆) → (0...(deg‘𝐹)) ∈ Fin) |
| 48 | 10, 25, 46, 47 | fsumss 15761 |
. 2
⊢ (𝐹 ∈ (Poly‘𝑆) → Σ𝑘 ∈ (0...0)((𝐴‘𝑘) · (0↑𝑘)) = Σ𝑘 ∈ (0...(deg‘𝐹))((𝐴‘𝑘) · (0↑𝑘))) |
| 49 | 22, 21 | eqeltrd 2841 |
. . . 4
⊢ (𝐹 ∈ (Poly‘𝑆) → ((𝐴‘0) · 1) ∈
ℂ) |
| 50 | 16 | fsum1 15783 |
. . . 4
⊢ ((0
∈ ℤ ∧ ((𝐴‘0) · 1) ∈ ℂ) →
Σ𝑘 ∈
(0...0)((𝐴‘𝑘) · (0↑𝑘)) = ((𝐴‘0) · 1)) |
| 51 | 34, 49, 50 | sylancr 587 |
. . 3
⊢ (𝐹 ∈ (Poly‘𝑆) → Σ𝑘 ∈ (0...0)((𝐴‘𝑘) · (0↑𝑘)) = ((𝐴‘0) · 1)) |
| 52 | 51, 22 | eqtrd 2777 |
. 2
⊢ (𝐹 ∈ (Poly‘𝑆) → Σ𝑘 ∈ (0...0)((𝐴‘𝑘) · (0↑𝑘)) = (𝐴‘0)) |
| 53 | 5, 48, 52 | 3eqtr2d 2783 |
1
⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹‘0) = (𝐴‘0)) |