# Metamath Proof Explorer

Description: Derive the coefficient function for the sum of two polynomials. (Contributed by Mario Carneiro, 23-Jul-2014)

Ref Expression
Hypotheses plyaddlem.1 ${⊢}{\phi }\to {F}\in \mathrm{Poly}\left({S}\right)$
plyaddlem.2 ${⊢}{\phi }\to {G}\in \mathrm{Poly}\left({S}\right)$
plyaddlem.m ${⊢}{\phi }\to {M}\in {ℕ}_{0}$
plyaddlem.n ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
plyaddlem.a ${⊢}{\phi }\to {A}:{ℕ}_{0}⟶ℂ$
plyaddlem.b ${⊢}{\phi }\to {B}:{ℕ}_{0}⟶ℂ$
plyaddlem.a2 ${⊢}{\phi }\to {A}\left[{ℤ}_{\ge \left({M}+1\right)}\right]=\left\{0\right\}$
plyaddlem.b2 ${⊢}{\phi }\to {B}\left[{ℤ}_{\ge \left({N}+1\right)}\right]=\left\{0\right\}$
plyaddlem.f ${⊢}{\phi }\to {F}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{M}}{A}\left({k}\right){{z}}^{{k}}\right)$
plyaddlem.g ${⊢}{\phi }\to {G}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{N}}{B}\left({k}\right){{z}}^{{k}}\right)$
Assertion plyaddlem1 ${⊢}{\phi }\to {F}{+}_{f}{G}=\left({z}\in ℂ⟼\sum _{{k}=0}^{if\left({M}\le {N},{N},{M}\right)}\left({A}{+}_{f}{B}\right)\left({k}\right){{z}}^{{k}}\right)$

### Proof

Step Hyp Ref Expression
1 plyaddlem.1 ${⊢}{\phi }\to {F}\in \mathrm{Poly}\left({S}\right)$
2 plyaddlem.2 ${⊢}{\phi }\to {G}\in \mathrm{Poly}\left({S}\right)$
3 plyaddlem.m ${⊢}{\phi }\to {M}\in {ℕ}_{0}$
4 plyaddlem.n ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
5 plyaddlem.a ${⊢}{\phi }\to {A}:{ℕ}_{0}⟶ℂ$
6 plyaddlem.b ${⊢}{\phi }\to {B}:{ℕ}_{0}⟶ℂ$
7 plyaddlem.a2 ${⊢}{\phi }\to {A}\left[{ℤ}_{\ge \left({M}+1\right)}\right]=\left\{0\right\}$
8 plyaddlem.b2 ${⊢}{\phi }\to {B}\left[{ℤ}_{\ge \left({N}+1\right)}\right]=\left\{0\right\}$
9 plyaddlem.f ${⊢}{\phi }\to {F}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{M}}{A}\left({k}\right){{z}}^{{k}}\right)$
10 plyaddlem.g ${⊢}{\phi }\to {G}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{N}}{B}\left({k}\right){{z}}^{{k}}\right)$
11 cnex ${⊢}ℂ\in \mathrm{V}$
12 11 a1i ${⊢}{\phi }\to ℂ\in \mathrm{V}$
13 sumex ${⊢}\sum _{{k}=0}^{{M}}{A}\left({k}\right){{z}}^{{k}}\in \mathrm{V}$
14 13 a1i ${⊢}\left({\phi }\wedge {z}\in ℂ\right)\to \sum _{{k}=0}^{{M}}{A}\left({k}\right){{z}}^{{k}}\in \mathrm{V}$
15 sumex ${⊢}\sum _{{k}=0}^{{N}}{B}\left({k}\right){{z}}^{{k}}\in \mathrm{V}$
16 15 a1i ${⊢}\left({\phi }\wedge {z}\in ℂ\right)\to \sum _{{k}=0}^{{N}}{B}\left({k}\right){{z}}^{{k}}\in \mathrm{V}$
17 12 14 16 9 10 offval2 ${⊢}{\phi }\to {F}{+}_{f}{G}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{M}}{A}\left({k}\right){{z}}^{{k}}+\sum _{{k}=0}^{{N}}{B}\left({k}\right){{z}}^{{k}}\right)$
18 fzfid ${⊢}\left({\phi }\wedge {z}\in ℂ\right)\to \left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\in \mathrm{Fin}$
19 elfznn0 ${⊢}{k}\in \left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\to {k}\in {ℕ}_{0}$
20 5 adantr ${⊢}\left({\phi }\wedge {z}\in ℂ\right)\to {A}:{ℕ}_{0}⟶ℂ$
21 20 ffvelrnda ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in {ℕ}_{0}\right)\to {A}\left({k}\right)\in ℂ$
22 expcl ${⊢}\left({z}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\to {{z}}^{{k}}\in ℂ$
23 22 adantll ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in {ℕ}_{0}\right)\to {{z}}^{{k}}\in ℂ$
24 21 23 mulcld ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in {ℕ}_{0}\right)\to {A}\left({k}\right){{z}}^{{k}}\in ℂ$
25 19 24 sylan2 ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\right)\to {A}\left({k}\right){{z}}^{{k}}\in ℂ$
26 6 adantr ${⊢}\left({\phi }\wedge {z}\in ℂ\right)\to {B}:{ℕ}_{0}⟶ℂ$
27 26 ffvelrnda ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in {ℕ}_{0}\right)\to {B}\left({k}\right)\in ℂ$
28 27 23 mulcld ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in {ℕ}_{0}\right)\to {B}\left({k}\right){{z}}^{{k}}\in ℂ$
29 19 28 sylan2 ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\right)\to {B}\left({k}\right){{z}}^{{k}}\in ℂ$
30 18 25 29 fsumadd ${⊢}\left({\phi }\wedge {z}\in ℂ\right)\to \sum _{{k}=0}^{if\left({M}\le {N},{N},{M}\right)}\left({A}\left({k}\right){{z}}^{{k}}+{B}\left({k}\right){{z}}^{{k}}\right)=\sum _{{k}=0}^{if\left({M}\le {N},{N},{M}\right)}{A}\left({k}\right){{z}}^{{k}}+\sum _{{k}=0}^{if\left({M}\le {N},{N},{M}\right)}{B}\left({k}\right){{z}}^{{k}}$
31 5 ffnd ${⊢}{\phi }\to {A}Fn{ℕ}_{0}$
32 6 ffnd ${⊢}{\phi }\to {B}Fn{ℕ}_{0}$
33 nn0ex ${⊢}{ℕ}_{0}\in \mathrm{V}$
34 33 a1i ${⊢}{\phi }\to {ℕ}_{0}\in \mathrm{V}$
35 inidm ${⊢}{ℕ}_{0}\cap {ℕ}_{0}={ℕ}_{0}$
36 eqidd ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to {A}\left({k}\right)={A}\left({k}\right)$
37 eqidd ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to {B}\left({k}\right)={B}\left({k}\right)$
38 31 32 34 34 35 36 37 ofval ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to \left({A}{+}_{f}{B}\right)\left({k}\right)={A}\left({k}\right)+{B}\left({k}\right)$
39 38 adantlr ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in {ℕ}_{0}\right)\to \left({A}{+}_{f}{B}\right)\left({k}\right)={A}\left({k}\right)+{B}\left({k}\right)$
40 39 oveq1d ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in {ℕ}_{0}\right)\to \left({A}{+}_{f}{B}\right)\left({k}\right){{z}}^{{k}}=\left({A}\left({k}\right)+{B}\left({k}\right)\right){{z}}^{{k}}$
41 21 27 23 adddird ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in {ℕ}_{0}\right)\to \left({A}\left({k}\right)+{B}\left({k}\right)\right){{z}}^{{k}}={A}\left({k}\right){{z}}^{{k}}+{B}\left({k}\right){{z}}^{{k}}$
42 40 41 eqtrd ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in {ℕ}_{0}\right)\to \left({A}{+}_{f}{B}\right)\left({k}\right){{z}}^{{k}}={A}\left({k}\right){{z}}^{{k}}+{B}\left({k}\right){{z}}^{{k}}$
43 19 42 sylan2 ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\right)\to \left({A}{+}_{f}{B}\right)\left({k}\right){{z}}^{{k}}={A}\left({k}\right){{z}}^{{k}}+{B}\left({k}\right){{z}}^{{k}}$
44 43 sumeq2dv ${⊢}\left({\phi }\wedge {z}\in ℂ\right)\to \sum _{{k}=0}^{if\left({M}\le {N},{N},{M}\right)}\left({A}{+}_{f}{B}\right)\left({k}\right){{z}}^{{k}}=\sum _{{k}=0}^{if\left({M}\le {N},{N},{M}\right)}\left({A}\left({k}\right){{z}}^{{k}}+{B}\left({k}\right){{z}}^{{k}}\right)$
45 3 nn0zd ${⊢}{\phi }\to {M}\in ℤ$
46 4 3 ifcld ${⊢}{\phi }\to if\left({M}\le {N},{N},{M}\right)\in {ℕ}_{0}$
47 46 nn0zd ${⊢}{\phi }\to if\left({M}\le {N},{N},{M}\right)\in ℤ$
48 3 nn0red ${⊢}{\phi }\to {M}\in ℝ$
49 4 nn0red ${⊢}{\phi }\to {N}\in ℝ$
50 max1 ${⊢}\left({M}\in ℝ\wedge {N}\in ℝ\right)\to {M}\le if\left({M}\le {N},{N},{M}\right)$
51 48 49 50 syl2anc ${⊢}{\phi }\to {M}\le if\left({M}\le {N},{N},{M}\right)$
52 eluz2 ${⊢}if\left({M}\le {N},{N},{M}\right)\in {ℤ}_{\ge {M}}↔\left({M}\in ℤ\wedge if\left({M}\le {N},{N},{M}\right)\in ℤ\wedge {M}\le if\left({M}\le {N},{N},{M}\right)\right)$
53 45 47 51 52 syl3anbrc ${⊢}{\phi }\to if\left({M}\le {N},{N},{M}\right)\in {ℤ}_{\ge {M}}$
54 fzss2 ${⊢}if\left({M}\le {N},{N},{M}\right)\in {ℤ}_{\ge {M}}\to \left(0\dots {M}\right)\subseteq \left(0\dots if\left({M}\le {N},{N},{M}\right)\right)$
55 53 54 syl ${⊢}{\phi }\to \left(0\dots {M}\right)\subseteq \left(0\dots if\left({M}\le {N},{N},{M}\right)\right)$
56 55 adantr ${⊢}\left({\phi }\wedge {z}\in ℂ\right)\to \left(0\dots {M}\right)\subseteq \left(0\dots if\left({M}\le {N},{N},{M}\right)\right)$
57 elfznn0 ${⊢}{k}\in \left(0\dots {M}\right)\to {k}\in {ℕ}_{0}$
58 57 24 sylan2 ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(0\dots {M}\right)\right)\to {A}\left({k}\right){{z}}^{{k}}\in ℂ$
59 eldifn ${⊢}{k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {M}\right)\right)\to ¬{k}\in \left(0\dots {M}\right)$
60 59 adantl ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {M}\right)\right)\right)\to ¬{k}\in \left(0\dots {M}\right)$
61 eldifi ${⊢}{k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {M}\right)\right)\to {k}\in \left(0\dots if\left({M}\le {N},{N},{M}\right)\right)$
62 61 19 syl ${⊢}{k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {M}\right)\right)\to {k}\in {ℕ}_{0}$
63 62 adantl ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {M}\right)\right)\right)\to {k}\in {ℕ}_{0}$
64 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
65 peano2nn0 ${⊢}{M}\in {ℕ}_{0}\to {M}+1\in {ℕ}_{0}$
66 3 65 syl ${⊢}{\phi }\to {M}+1\in {ℕ}_{0}$
67 66 64 eleqtrdi ${⊢}{\phi }\to {M}+1\in {ℤ}_{\ge 0}$
68 uzsplit ${⊢}{M}+1\in {ℤ}_{\ge 0}\to {ℤ}_{\ge 0}=\left(0\dots {M}+1-1\right)\cup {ℤ}_{\ge \left({M}+1\right)}$
69 67 68 syl ${⊢}{\phi }\to {ℤ}_{\ge 0}=\left(0\dots {M}+1-1\right)\cup {ℤ}_{\ge \left({M}+1\right)}$
70 64 69 syl5eq ${⊢}{\phi }\to {ℕ}_{0}=\left(0\dots {M}+1-1\right)\cup {ℤ}_{\ge \left({M}+1\right)}$
71 3 nn0cnd ${⊢}{\phi }\to {M}\in ℂ$
72 ax-1cn ${⊢}1\in ℂ$
73 pncan ${⊢}\left({M}\in ℂ\wedge 1\in ℂ\right)\to {M}+1-1={M}$
74 71 72 73 sylancl ${⊢}{\phi }\to {M}+1-1={M}$
75 74 oveq2d ${⊢}{\phi }\to \left(0\dots {M}+1-1\right)=\left(0\dots {M}\right)$
76 75 uneq1d ${⊢}{\phi }\to \left(0\dots {M}+1-1\right)\cup {ℤ}_{\ge \left({M}+1\right)}=\left(0\dots {M}\right)\cup {ℤ}_{\ge \left({M}+1\right)}$
77 70 76 eqtrd ${⊢}{\phi }\to {ℕ}_{0}=\left(0\dots {M}\right)\cup {ℤ}_{\ge \left({M}+1\right)}$
78 77 ad2antrr ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {M}\right)\right)\right)\to {ℕ}_{0}=\left(0\dots {M}\right)\cup {ℤ}_{\ge \left({M}+1\right)}$
79 63 78 eleqtrd ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {M}\right)\right)\right)\to {k}\in \left(\left(0\dots {M}\right)\cup {ℤ}_{\ge \left({M}+1\right)}\right)$
80 elun ${⊢}{k}\in \left(\left(0\dots {M}\right)\cup {ℤ}_{\ge \left({M}+1\right)}\right)↔\left({k}\in \left(0\dots {M}\right)\vee {k}\in {ℤ}_{\ge \left({M}+1\right)}\right)$
81 79 80 sylib ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {M}\right)\right)\right)\to \left({k}\in \left(0\dots {M}\right)\vee {k}\in {ℤ}_{\ge \left({M}+1\right)}\right)$
82 81 ord ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {M}\right)\right)\right)\to \left(¬{k}\in \left(0\dots {M}\right)\to {k}\in {ℤ}_{\ge \left({M}+1\right)}\right)$
83 60 82 mpd ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {M}\right)\right)\right)\to {k}\in {ℤ}_{\ge \left({M}+1\right)}$
84 5 ffund ${⊢}{\phi }\to \mathrm{Fun}{A}$
85 ssun2 ${⊢}{ℤ}_{\ge \left({M}+1\right)}\subseteq \left(0\dots {M}+1-1\right)\cup {ℤ}_{\ge \left({M}+1\right)}$
86 85 70 sseqtrrid ${⊢}{\phi }\to {ℤ}_{\ge \left({M}+1\right)}\subseteq {ℕ}_{0}$
87 5 fdmd ${⊢}{\phi }\to \mathrm{dom}{A}={ℕ}_{0}$
88 86 87 sseqtrrd ${⊢}{\phi }\to {ℤ}_{\ge \left({M}+1\right)}\subseteq \mathrm{dom}{A}$
89 funfvima2 ${⊢}\left(\mathrm{Fun}{A}\wedge {ℤ}_{\ge \left({M}+1\right)}\subseteq \mathrm{dom}{A}\right)\to \left({k}\in {ℤ}_{\ge \left({M}+1\right)}\to {A}\left({k}\right)\in {A}\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)$
90 84 88 89 syl2anc ${⊢}{\phi }\to \left({k}\in {ℤ}_{\ge \left({M}+1\right)}\to {A}\left({k}\right)\in {A}\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)$
91 90 ad2antrr ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {M}\right)\right)\right)\to \left({k}\in {ℤ}_{\ge \left({M}+1\right)}\to {A}\left({k}\right)\in {A}\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)$
92 83 91 mpd ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {M}\right)\right)\right)\to {A}\left({k}\right)\in {A}\left[{ℤ}_{\ge \left({M}+1\right)}\right]$
93 7 ad2antrr ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {M}\right)\right)\right)\to {A}\left[{ℤ}_{\ge \left({M}+1\right)}\right]=\left\{0\right\}$
94 92 93 eleqtrd ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {M}\right)\right)\right)\to {A}\left({k}\right)\in \left\{0\right\}$
95 elsni ${⊢}{A}\left({k}\right)\in \left\{0\right\}\to {A}\left({k}\right)=0$
96 94 95 syl ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {M}\right)\right)\right)\to {A}\left({k}\right)=0$
97 96 oveq1d ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {M}\right)\right)\right)\to {A}\left({k}\right){{z}}^{{k}}=0\cdot {{z}}^{{k}}$
98 62 23 sylan2 ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {M}\right)\right)\right)\to {{z}}^{{k}}\in ℂ$
99 98 mul02d ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {M}\right)\right)\right)\to 0\cdot {{z}}^{{k}}=0$
100 97 99 eqtrd ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {M}\right)\right)\right)\to {A}\left({k}\right){{z}}^{{k}}=0$
101 56 58 100 18 fsumss ${⊢}\left({\phi }\wedge {z}\in ℂ\right)\to \sum _{{k}=0}^{{M}}{A}\left({k}\right){{z}}^{{k}}=\sum _{{k}=0}^{if\left({M}\le {N},{N},{M}\right)}{A}\left({k}\right){{z}}^{{k}}$
102 4 nn0zd ${⊢}{\phi }\to {N}\in ℤ$
103 max2 ${⊢}\left({M}\in ℝ\wedge {N}\in ℝ\right)\to {N}\le if\left({M}\le {N},{N},{M}\right)$
104 48 49 103 syl2anc ${⊢}{\phi }\to {N}\le if\left({M}\le {N},{N},{M}\right)$
105 eluz2 ${⊢}if\left({M}\le {N},{N},{M}\right)\in {ℤ}_{\ge {N}}↔\left({N}\in ℤ\wedge if\left({M}\le {N},{N},{M}\right)\in ℤ\wedge {N}\le if\left({M}\le {N},{N},{M}\right)\right)$
106 102 47 104 105 syl3anbrc ${⊢}{\phi }\to if\left({M}\le {N},{N},{M}\right)\in {ℤ}_{\ge {N}}$
107 fzss2 ${⊢}if\left({M}\le {N},{N},{M}\right)\in {ℤ}_{\ge {N}}\to \left(0\dots {N}\right)\subseteq \left(0\dots if\left({M}\le {N},{N},{M}\right)\right)$
108 106 107 syl ${⊢}{\phi }\to \left(0\dots {N}\right)\subseteq \left(0\dots if\left({M}\le {N},{N},{M}\right)\right)$
109 108 adantr ${⊢}\left({\phi }\wedge {z}\in ℂ\right)\to \left(0\dots {N}\right)\subseteq \left(0\dots if\left({M}\le {N},{N},{M}\right)\right)$
110 elfznn0 ${⊢}{k}\in \left(0\dots {N}\right)\to {k}\in {ℕ}_{0}$
111 110 28 sylan2 ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(0\dots {N}\right)\right)\to {B}\left({k}\right){{z}}^{{k}}\in ℂ$
112 eldifn ${⊢}{k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {N}\right)\right)\to ¬{k}\in \left(0\dots {N}\right)$
113 112 adantl ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {N}\right)\right)\right)\to ¬{k}\in \left(0\dots {N}\right)$
114 eldifi ${⊢}{k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {N}\right)\right)\to {k}\in \left(0\dots if\left({M}\le {N},{N},{M}\right)\right)$
115 114 19 syl ${⊢}{k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {N}\right)\right)\to {k}\in {ℕ}_{0}$
116 115 adantl ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {N}\right)\right)\right)\to {k}\in {ℕ}_{0}$
117 peano2nn0 ${⊢}{N}\in {ℕ}_{0}\to {N}+1\in {ℕ}_{0}$
118 4 117 syl ${⊢}{\phi }\to {N}+1\in {ℕ}_{0}$
119 118 64 eleqtrdi ${⊢}{\phi }\to {N}+1\in {ℤ}_{\ge 0}$
120 uzsplit ${⊢}{N}+1\in {ℤ}_{\ge 0}\to {ℤ}_{\ge 0}=\left(0\dots {N}+1-1\right)\cup {ℤ}_{\ge \left({N}+1\right)}$
121 119 120 syl ${⊢}{\phi }\to {ℤ}_{\ge 0}=\left(0\dots {N}+1-1\right)\cup {ℤ}_{\ge \left({N}+1\right)}$
122 64 121 syl5eq ${⊢}{\phi }\to {ℕ}_{0}=\left(0\dots {N}+1-1\right)\cup {ℤ}_{\ge \left({N}+1\right)}$
123 4 nn0cnd ${⊢}{\phi }\to {N}\in ℂ$
124 pncan ${⊢}\left({N}\in ℂ\wedge 1\in ℂ\right)\to {N}+1-1={N}$
125 123 72 124 sylancl ${⊢}{\phi }\to {N}+1-1={N}$
126 125 oveq2d ${⊢}{\phi }\to \left(0\dots {N}+1-1\right)=\left(0\dots {N}\right)$
127 126 uneq1d ${⊢}{\phi }\to \left(0\dots {N}+1-1\right)\cup {ℤ}_{\ge \left({N}+1\right)}=\left(0\dots {N}\right)\cup {ℤ}_{\ge \left({N}+1\right)}$
128 122 127 eqtrd ${⊢}{\phi }\to {ℕ}_{0}=\left(0\dots {N}\right)\cup {ℤ}_{\ge \left({N}+1\right)}$
129 128 ad2antrr ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {N}\right)\right)\right)\to {ℕ}_{0}=\left(0\dots {N}\right)\cup {ℤ}_{\ge \left({N}+1\right)}$
130 116 129 eleqtrd ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {N}\right)\right)\right)\to {k}\in \left(\left(0\dots {N}\right)\cup {ℤ}_{\ge \left({N}+1\right)}\right)$
131 elun ${⊢}{k}\in \left(\left(0\dots {N}\right)\cup {ℤ}_{\ge \left({N}+1\right)}\right)↔\left({k}\in \left(0\dots {N}\right)\vee {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)$
132 130 131 sylib ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {N}\right)\right)\right)\to \left({k}\in \left(0\dots {N}\right)\vee {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)$
133 132 ord ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {N}\right)\right)\right)\to \left(¬{k}\in \left(0\dots {N}\right)\to {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)$
134 113 133 mpd ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {N}\right)\right)\right)\to {k}\in {ℤ}_{\ge \left({N}+1\right)}$
135 6 ffund ${⊢}{\phi }\to \mathrm{Fun}{B}$
136 ssun2 ${⊢}{ℤ}_{\ge \left({N}+1\right)}\subseteq \left(0\dots {N}+1-1\right)\cup {ℤ}_{\ge \left({N}+1\right)}$
137 136 122 sseqtrrid ${⊢}{\phi }\to {ℤ}_{\ge \left({N}+1\right)}\subseteq {ℕ}_{0}$
138 6 fdmd ${⊢}{\phi }\to \mathrm{dom}{B}={ℕ}_{0}$
139 137 138 sseqtrrd ${⊢}{\phi }\to {ℤ}_{\ge \left({N}+1\right)}\subseteq \mathrm{dom}{B}$
140 funfvima2 ${⊢}\left(\mathrm{Fun}{B}\wedge {ℤ}_{\ge \left({N}+1\right)}\subseteq \mathrm{dom}{B}\right)\to \left({k}\in {ℤ}_{\ge \left({N}+1\right)}\to {B}\left({k}\right)\in {B}\left[{ℤ}_{\ge \left({N}+1\right)}\right]\right)$
141 135 139 140 syl2anc ${⊢}{\phi }\to \left({k}\in {ℤ}_{\ge \left({N}+1\right)}\to {B}\left({k}\right)\in {B}\left[{ℤ}_{\ge \left({N}+1\right)}\right]\right)$
142 141 ad2antrr ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {N}\right)\right)\right)\to \left({k}\in {ℤ}_{\ge \left({N}+1\right)}\to {B}\left({k}\right)\in {B}\left[{ℤ}_{\ge \left({N}+1\right)}\right]\right)$
143 134 142 mpd ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {N}\right)\right)\right)\to {B}\left({k}\right)\in {B}\left[{ℤ}_{\ge \left({N}+1\right)}\right]$
144 8 ad2antrr ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {N}\right)\right)\right)\to {B}\left[{ℤ}_{\ge \left({N}+1\right)}\right]=\left\{0\right\}$
145 143 144 eleqtrd ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {N}\right)\right)\right)\to {B}\left({k}\right)\in \left\{0\right\}$
146 elsni ${⊢}{B}\left({k}\right)\in \left\{0\right\}\to {B}\left({k}\right)=0$
147 145 146 syl ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {N}\right)\right)\right)\to {B}\left({k}\right)=0$
148 147 oveq1d ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {N}\right)\right)\right)\to {B}\left({k}\right){{z}}^{{k}}=0\cdot {{z}}^{{k}}$
149 115 23 sylan2 ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {N}\right)\right)\right)\to {{z}}^{{k}}\in ℂ$
150 149 mul02d ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {N}\right)\right)\right)\to 0\cdot {{z}}^{{k}}=0$
151 148 150 eqtrd ${⊢}\left(\left({\phi }\wedge {z}\in ℂ\right)\wedge {k}\in \left(\left(0\dots if\left({M}\le {N},{N},{M}\right)\right)\setminus \left(0\dots {N}\right)\right)\right)\to {B}\left({k}\right){{z}}^{{k}}=0$
152 109 111 151 18 fsumss ${⊢}\left({\phi }\wedge {z}\in ℂ\right)\to \sum _{{k}=0}^{{N}}{B}\left({k}\right){{z}}^{{k}}=\sum _{{k}=0}^{if\left({M}\le {N},{N},{M}\right)}{B}\left({k}\right){{z}}^{{k}}$
153 101 152 oveq12d ${⊢}\left({\phi }\wedge {z}\in ℂ\right)\to \sum _{{k}=0}^{{M}}{A}\left({k}\right){{z}}^{{k}}+\sum _{{k}=0}^{{N}}{B}\left({k}\right){{z}}^{{k}}=\sum _{{k}=0}^{if\left({M}\le {N},{N},{M}\right)}{A}\left({k}\right){{z}}^{{k}}+\sum _{{k}=0}^{if\left({M}\le {N},{N},{M}\right)}{B}\left({k}\right){{z}}^{{k}}$
154 30 44 153 3eqtr4d ${⊢}\left({\phi }\wedge {z}\in ℂ\right)\to \sum _{{k}=0}^{if\left({M}\le {N},{N},{M}\right)}\left({A}{+}_{f}{B}\right)\left({k}\right){{z}}^{{k}}=\sum _{{k}=0}^{{M}}{A}\left({k}\right){{z}}^{{k}}+\sum _{{k}=0}^{{N}}{B}\left({k}\right){{z}}^{{k}}$
155 154 mpteq2dva ${⊢}{\phi }\to \left({z}\in ℂ⟼\sum _{{k}=0}^{if\left({M}\le {N},{N},{M}\right)}\left({A}{+}_{f}{B}\right)\left({k}\right){{z}}^{{k}}\right)=\left({z}\in ℂ⟼\sum _{{k}=0}^{{M}}{A}\left({k}\right){{z}}^{{k}}+\sum _{{k}=0}^{{N}}{B}\left({k}\right){{z}}^{{k}}\right)$
156 17 155 eqtr4d ${⊢}{\phi }\to {F}{+}_{f}{G}=\left({z}\in ℂ⟼\sum _{{k}=0}^{if\left({M}\le {N},{N},{M}\right)}\left({A}{+}_{f}{B}\right)\left({k}\right){{z}}^{{k}}\right)$