plyaddlem1

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

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

Proof

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

Metamath Proof Explorer

Theorem plyaddlem1

Proof