Step | Hyp | Ref
| Expression |
1 | | ssid 3587 |
. . . . 5
⊢ ℂ
⊆ ℂ |
2 | | plyconst 23766 |
. . . . 5
⊢ ((ℂ
⊆ ℂ ∧ 𝐴
∈ ℂ) → (ℂ × {𝐴}) ∈
(Poly‘ℂ)) |
3 | 1, 2 | mpan 702 |
. . . 4
⊢ (𝐴 ∈ ℂ → (ℂ
× {𝐴}) ∈
(Poly‘ℂ)) |
4 | | plyssc 23760 |
. . . . 5
⊢
(Poly‘𝑆)
⊆ (Poly‘ℂ) |
5 | 4 | sseli 3564 |
. . . 4
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹 ∈
(Poly‘ℂ)) |
6 | | plymulcl 23781 |
. . . 4
⊢
(((ℂ × {𝐴}) ∈ (Poly‘ℂ) ∧ 𝐹 ∈ (Poly‘ℂ))
→ ((ℂ × {𝐴}) ∘𝑓 ·
𝐹) ∈
(Poly‘ℂ)) |
7 | 3, 5, 6 | syl2an 493 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) → ((ℂ ×
{𝐴})
∘𝑓 · 𝐹) ∈
(Poly‘ℂ)) |
8 | | eqid 2610 |
. . . 4
⊢
(coeff‘((ℂ × {𝐴}) ∘𝑓 ·
𝐹)) =
(coeff‘((ℂ × {𝐴}) ∘𝑓 ·
𝐹)) |
9 | 8 | coef3 23792 |
. . 3
⊢
(((ℂ × {𝐴}) ∘𝑓 ·
𝐹) ∈
(Poly‘ℂ) → (coeff‘((ℂ × {𝐴}) ∘𝑓 ·
𝐹)):ℕ0⟶ℂ) |
10 | | ffn 5958 |
. . 3
⊢
((coeff‘((ℂ × {𝐴}) ∘𝑓 ·
𝐹)):ℕ0⟶ℂ →
(coeff‘((ℂ × {𝐴}) ∘𝑓 ·
𝐹)) Fn
ℕ0) |
11 | 7, 9, 10 | 3syl 18 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) → (coeff‘((ℂ
× {𝐴})
∘𝑓 · 𝐹)) Fn ℕ0) |
12 | | fconstg 6005 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
(ℕ0 × {𝐴}):ℕ0⟶{𝐴}) |
13 | 12 | adantr 480 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) → (ℕ0
× {𝐴}):ℕ0⟶{𝐴}) |
14 | | ffn 5958 |
. . . 4
⊢
((ℕ0 × {𝐴}):ℕ0⟶{𝐴} → (ℕ0
× {𝐴}) Fn
ℕ0) |
15 | 13, 14 | syl 17 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) → (ℕ0
× {𝐴}) Fn
ℕ0) |
16 | | eqid 2610 |
. . . . . 6
⊢
(coeff‘𝐹) =
(coeff‘𝐹) |
17 | 16 | coef3 23792 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘𝑆) → (coeff‘𝐹):ℕ0⟶ℂ) |
18 | 17 | adantl 481 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) → (coeff‘𝐹):ℕ0⟶ℂ) |
19 | | ffn 5958 |
. . . 4
⊢
((coeff‘𝐹):ℕ0⟶ℂ →
(coeff‘𝐹) Fn
ℕ0) |
20 | 18, 19 | syl 17 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) → (coeff‘𝐹) Fn
ℕ0) |
21 | | nn0ex 11175 |
. . . 4
⊢
ℕ0 ∈ V |
22 | 21 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) → ℕ0
∈ V) |
23 | | inidm 3784 |
. . 3
⊢
(ℕ0 ∩ ℕ0) =
ℕ0 |
24 | 15, 20, 22, 22, 23 | offn 6806 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) → ((ℕ0
× {𝐴})
∘𝑓 · (coeff‘𝐹)) Fn ℕ0) |
25 | 3 | ad2antrr 758 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) → (ℂ
× {𝐴}) ∈
(Poly‘ℂ)) |
26 | | eqid 2610 |
. . . . . . 7
⊢
(coeff‘(ℂ × {𝐴})) = (coeff‘(ℂ × {𝐴})) |
27 | 26 | coefv0 23808 |
. . . . . 6
⊢ ((ℂ
× {𝐴}) ∈
(Poly‘ℂ) → ((ℂ × {𝐴})‘0) = ((coeff‘(ℂ ×
{𝐴}))‘0)) |
28 | 25, 27 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) → ((ℂ
× {𝐴})‘0) =
((coeff‘(ℂ × {𝐴}))‘0)) |
29 | | simpll 786 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) → 𝐴 ∈
ℂ) |
30 | | 0cn 9911 |
. . . . . 6
⊢ 0 ∈
ℂ |
31 | | fvconst2g 6372 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 0 ∈
ℂ) → ((ℂ × {𝐴})‘0) = 𝐴) |
32 | 29, 30, 31 | sylancl 693 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) → ((ℂ
× {𝐴})‘0) =
𝐴) |
33 | 28, 32 | eqtr3d 2646 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) →
((coeff‘(ℂ × {𝐴}))‘0) = 𝐴) |
34 | | simpr 476 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
ℕ0) |
35 | 34 | nn0cnd 11230 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
ℂ) |
36 | 35 | subid1d 10260 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) → (𝑛 − 0) = 𝑛) |
37 | 36 | fveq2d 6107 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) →
((coeff‘𝐹)‘(𝑛 − 0)) = ((coeff‘𝐹)‘𝑛)) |
38 | 33, 37 | oveq12d 6567 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) →
(((coeff‘(ℂ × {𝐴}))‘0) · ((coeff‘𝐹)‘(𝑛 − 0))) = (𝐴 · ((coeff‘𝐹)‘𝑛))) |
39 | 5 | ad2antlr 759 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) → 𝐹 ∈
(Poly‘ℂ)) |
40 | 26, 16 | coemul 23812 |
. . . . 5
⊢
(((ℂ × {𝐴}) ∈ (Poly‘ℂ) ∧ 𝐹 ∈ (Poly‘ℂ)
∧ 𝑛 ∈
ℕ0) → ((coeff‘((ℂ × {𝐴}) ∘𝑓 ·
𝐹))‘𝑛) = Σ𝑘 ∈ (0...𝑛)(((coeff‘(ℂ × {𝐴}))‘𝑘) · ((coeff‘𝐹)‘(𝑛 − 𝑘)))) |
41 | 25, 39, 34, 40 | syl3anc 1318 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) →
((coeff‘((ℂ × {𝐴}) ∘𝑓 ·
𝐹))‘𝑛) = Σ𝑘 ∈ (0...𝑛)(((coeff‘(ℂ × {𝐴}))‘𝑘) · ((coeff‘𝐹)‘(𝑛 − 𝑘)))) |
42 | | nn0uz 11598 |
. . . . . . 7
⊢
ℕ0 = (ℤ≥‘0) |
43 | 34, 42 | syl6eleq 2698 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
(ℤ≥‘0)) |
44 | | fzss2 12252 |
. . . . . 6
⊢ (𝑛 ∈
(ℤ≥‘0) → (0...0) ⊆ (0...𝑛)) |
45 | 43, 44 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) → (0...0)
⊆ (0...𝑛)) |
46 | | elfz1eq 12223 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...0) → 𝑘 = 0) |
47 | 46 | adantl 481 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ (0...0)) → 𝑘 = 0) |
48 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑘 = 0 →
((coeff‘(ℂ × {𝐴}))‘𝑘) = ((coeff‘(ℂ × {𝐴}))‘0)) |
49 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑘 = 0 → (𝑛 − 𝑘) = (𝑛 − 0)) |
50 | 49 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑘 = 0 → ((coeff‘𝐹)‘(𝑛 − 𝑘)) = ((coeff‘𝐹)‘(𝑛 − 0))) |
51 | 48, 50 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑘 = 0 →
(((coeff‘(ℂ × {𝐴}))‘𝑘) · ((coeff‘𝐹)‘(𝑛 − 𝑘))) = (((coeff‘(ℂ × {𝐴}))‘0) ·
((coeff‘𝐹)‘(𝑛 − 0)))) |
52 | 47, 51 | syl 17 |
. . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ (0...0)) →
(((coeff‘(ℂ × {𝐴}))‘𝑘) · ((coeff‘𝐹)‘(𝑛 − 𝑘))) = (((coeff‘(ℂ × {𝐴}))‘0) ·
((coeff‘𝐹)‘(𝑛 − 0)))) |
53 | 18 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) →
((coeff‘𝐹)‘𝑛) ∈ ℂ) |
54 | 29, 53 | mulcld 9939 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) → (𝐴 · ((coeff‘𝐹)‘𝑛)) ∈ ℂ) |
55 | 38, 54 | eqeltrd 2688 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) →
(((coeff‘(ℂ × {𝐴}))‘0) · ((coeff‘𝐹)‘(𝑛 − 0))) ∈
ℂ) |
56 | 55 | adantr 480 |
. . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ (0...0)) →
(((coeff‘(ℂ × {𝐴}))‘0) · ((coeff‘𝐹)‘(𝑛 − 0))) ∈
ℂ) |
57 | 52, 56 | eqeltrd 2688 |
. . . . 5
⊢ ((((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ (0...0)) →
(((coeff‘(ℂ × {𝐴}))‘𝑘) · ((coeff‘𝐹)‘(𝑛 − 𝑘))) ∈ ℂ) |
58 | | eldifn 3695 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((0...𝑛) ∖ (0...0)) → ¬ 𝑘 ∈
(0...0)) |
59 | 58 | adantl 481 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ((0...𝑛) ∖ (0...0))) → ¬ 𝑘 ∈
(0...0)) |
60 | | eldifi 3694 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ((0...𝑛) ∖ (0...0)) → 𝑘 ∈ (0...𝑛)) |
61 | | elfznn0 12302 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (0...𝑛) → 𝑘 ∈ ℕ0) |
62 | 60, 61 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ((0...𝑛) ∖ (0...0)) → 𝑘 ∈ ℕ0) |
63 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(deg‘(ℂ × {𝐴})) = (deg‘(ℂ × {𝐴})) |
64 | 26, 63 | dgrub 23794 |
. . . . . . . . . . . . 13
⊢
(((ℂ × {𝐴}) ∈ (Poly‘ℂ) ∧ 𝑘 ∈ ℕ0
∧ ((coeff‘(ℂ × {𝐴}))‘𝑘) ≠ 0) → 𝑘 ≤ (deg‘(ℂ × {𝐴}))) |
65 | 64 | 3expia 1259 |
. . . . . . . . . . . 12
⊢
(((ℂ × {𝐴}) ∈ (Poly‘ℂ) ∧ 𝑘 ∈ ℕ0)
→ (((coeff‘(ℂ × {𝐴}))‘𝑘) ≠ 0 → 𝑘 ≤ (deg‘(ℂ × {𝐴})))) |
66 | 25, 62, 65 | syl2an 493 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ((0...𝑛) ∖ (0...0))) →
(((coeff‘(ℂ × {𝐴}))‘𝑘) ≠ 0 → 𝑘 ≤ (deg‘(ℂ × {𝐴})))) |
67 | | 0dgr 23805 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
(deg‘(ℂ × {𝐴})) = 0) |
68 | 67 | ad3antrrr 762 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ((0...𝑛) ∖ (0...0))) →
(deg‘(ℂ × {𝐴})) = 0) |
69 | 68 | breq2d 4595 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ((0...𝑛) ∖ (0...0))) → (𝑘 ≤ (deg‘(ℂ
× {𝐴})) ↔ 𝑘 ≤ 0)) |
70 | 62 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ((0...𝑛) ∖ (0...0))) → 𝑘 ∈ ℕ0) |
71 | | nn0le0eq0 11198 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ0
→ (𝑘 ≤ 0 ↔
𝑘 = 0)) |
72 | 70, 71 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ((0...𝑛) ∖ (0...0))) → (𝑘 ≤ 0 ↔ 𝑘 = 0)) |
73 | 69, 72 | bitrd 267 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ((0...𝑛) ∖ (0...0))) → (𝑘 ≤ (deg‘(ℂ
× {𝐴})) ↔ 𝑘 = 0)) |
74 | 66, 73 | sylibd 228 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ((0...𝑛) ∖ (0...0))) →
(((coeff‘(ℂ × {𝐴}))‘𝑘) ≠ 0 → 𝑘 = 0)) |
75 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑘 = 0 → 𝑘 = 0) |
76 | | 0z 11265 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℤ |
77 | | elfz3 12222 |
. . . . . . . . . . . 12
⊢ (0 ∈
ℤ → 0 ∈ (0...0)) |
78 | 76, 77 | ax-mp 5 |
. . . . . . . . . . 11
⊢ 0 ∈
(0...0) |
79 | 75, 78 | syl6eqel 2696 |
. . . . . . . . . 10
⊢ (𝑘 = 0 → 𝑘 ∈ (0...0)) |
80 | 74, 79 | syl6 34 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ((0...𝑛) ∖ (0...0))) →
(((coeff‘(ℂ × {𝐴}))‘𝑘) ≠ 0 → 𝑘 ∈ (0...0))) |
81 | 80 | necon1bd 2800 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ((0...𝑛) ∖ (0...0))) → (¬ 𝑘 ∈ (0...0) →
((coeff‘(ℂ × {𝐴}))‘𝑘) = 0)) |
82 | 59, 81 | mpd 15 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ((0...𝑛) ∖ (0...0))) →
((coeff‘(ℂ × {𝐴}))‘𝑘) = 0) |
83 | 82 | oveq1d 6564 |
. . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ((0...𝑛) ∖ (0...0))) →
(((coeff‘(ℂ × {𝐴}))‘𝑘) · ((coeff‘𝐹)‘(𝑛 − 𝑘))) = (0 · ((coeff‘𝐹)‘(𝑛 − 𝑘)))) |
84 | 18 | adantr 480 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) →
(coeff‘𝐹):ℕ0⟶ℂ) |
85 | | fznn0sub 12244 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...𝑛) → (𝑛 − 𝑘) ∈
ℕ0) |
86 | 60, 85 | syl 17 |
. . . . . . . 8
⊢ (𝑘 ∈ ((0...𝑛) ∖ (0...0)) → (𝑛 − 𝑘) ∈
ℕ0) |
87 | | ffvelrn 6265 |
. . . . . . . 8
⊢
(((coeff‘𝐹):ℕ0⟶ℂ ∧
(𝑛 − 𝑘) ∈ ℕ0)
→ ((coeff‘𝐹)‘(𝑛 − 𝑘)) ∈ ℂ) |
88 | 84, 86, 87 | syl2an 493 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ((0...𝑛) ∖ (0...0))) →
((coeff‘𝐹)‘(𝑛 − 𝑘)) ∈ ℂ) |
89 | 88 | mul02d 10113 |
. . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ((0...𝑛) ∖ (0...0))) → (0 ·
((coeff‘𝐹)‘(𝑛 − 𝑘))) = 0) |
90 | 83, 89 | eqtrd 2644 |
. . . . 5
⊢ ((((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ((0...𝑛) ∖ (0...0))) →
(((coeff‘(ℂ × {𝐴}))‘𝑘) · ((coeff‘𝐹)‘(𝑛 − 𝑘))) = 0) |
91 | | fzfid 12634 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) →
(0...𝑛) ∈
Fin) |
92 | 45, 57, 90, 91 | fsumss 14303 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) →
Σ𝑘 ∈
(0...0)(((coeff‘(ℂ × {𝐴}))‘𝑘) · ((coeff‘𝐹)‘(𝑛 − 𝑘))) = Σ𝑘 ∈ (0...𝑛)(((coeff‘(ℂ × {𝐴}))‘𝑘) · ((coeff‘𝐹)‘(𝑛 − 𝑘)))) |
93 | 51 | fsum1 14320 |
. . . . 5
⊢ ((0
∈ ℤ ∧ (((coeff‘(ℂ × {𝐴}))‘0) · ((coeff‘𝐹)‘(𝑛 − 0))) ∈ ℂ) →
Σ𝑘 ∈
(0...0)(((coeff‘(ℂ × {𝐴}))‘𝑘) · ((coeff‘𝐹)‘(𝑛 − 𝑘))) = (((coeff‘(ℂ × {𝐴}))‘0) ·
((coeff‘𝐹)‘(𝑛 − 0)))) |
94 | 76, 55, 93 | sylancr 694 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) →
Σ𝑘 ∈
(0...0)(((coeff‘(ℂ × {𝐴}))‘𝑘) · ((coeff‘𝐹)‘(𝑛 − 𝑘))) = (((coeff‘(ℂ × {𝐴}))‘0) ·
((coeff‘𝐹)‘(𝑛 − 0)))) |
95 | 41, 92, 94 | 3eqtr2d 2650 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) →
((coeff‘((ℂ × {𝐴}) ∘𝑓 ·
𝐹))‘𝑛) = (((coeff‘(ℂ
× {𝐴}))‘0)
· ((coeff‘𝐹)‘(𝑛 − 0)))) |
96 | | simpl 472 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) → 𝐴 ∈ ℂ) |
97 | | eqidd 2611 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) →
((coeff‘𝐹)‘𝑛) = ((coeff‘𝐹)‘𝑛)) |
98 | 22, 96, 20, 97 | ofc1 6818 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) →
(((ℕ0 × {𝐴}) ∘𝑓 ·
(coeff‘𝐹))‘𝑛) = (𝐴 · ((coeff‘𝐹)‘𝑛))) |
99 | 38, 95, 98 | 3eqtr4d 2654 |
. 2
⊢ (((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ0) →
((coeff‘((ℂ × {𝐴}) ∘𝑓 ·
𝐹))‘𝑛) = (((ℕ0
× {𝐴})
∘𝑓 · (coeff‘𝐹))‘𝑛)) |
100 | 11, 24, 99 | eqfnfvd 6222 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) → (coeff‘((ℂ
× {𝐴})
∘𝑓 · 𝐹)) = ((ℕ0 × {𝐴}) ∘𝑓
· (coeff‘𝐹))) |