plymullem1

Description: Derive the coefficient function for the product 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	plymullem1	$⊢ φ \to F \times_{f} G = (z \in ℂ ⟼ \sum_{n = 0}^{M + N} \sum_{k = 0}^{n} A (k) B (n - k) z^{n})$

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 \times_{f} G = (z \in ℂ ⟼ \sum_{k = 0}^{M} A (k) z^{k} \sum_{k = 0}^{N} B (k) z^{k})$
18		fveq2	$⊢ m = n \to B (m) = B (n)$
19		oveq2	$⊢ m = n \to z^{m} = z^{n}$
20	18 19	oveq12d	$⊢ m = n \to B (m) z^{m} = B (n) z^{n}$
21	20	oveq2d	$⊢ m = n \to A (k) z^{k} B (m) z^{m} = A (k) z^{k} B (n) z^{n}$
22		fveq2	$⊢ m = n - k \to B (m) = B (n - k)$
23		oveq2	$⊢ m = n - k \to z^{m} = z^{n - k}$
24	22 23	oveq12d	$⊢ m = n - k \to B (m) z^{m} = B (n - k) z^{n - k}$
25	24	oveq2d	$⊢ m = n - k \to A (k) z^{k} B (m) z^{m} = A (k) z^{k} B (n - k) z^{n - k}$
26		elfznn0	$⊢ k \in (0 \dots M + N) \to k \in ℕ_{0}$
27	5	adantr	$⊢ (φ \land z \in ℂ) \to A : ℕ_{0} ⟶ ℂ$
28	27	ffvelrnda	$⊢ ((φ \land z \in ℂ) \land k \in ℕ_{0}) \to A (k) \in ℂ$
29		expcl	$⊢ (z \in ℂ \land k \in ℕ_{0}) \to z^{k} \in ℂ$
30	29	adantll	$⊢ ((φ \land z \in ℂ) \land k \in ℕ_{0}) \to z^{k} \in ℂ$
31	28 30	mulcld	$⊢ ((φ \land z \in ℂ) \land k \in ℕ_{0}) \to A (k) z^{k} \in ℂ$
32	26 31	sylan2	$⊢ ((φ \land z \in ℂ) \land k \in (0 \dots M + N)) \to A (k) z^{k} \in ℂ$
33		elfznn0	$⊢ n \in (0 \dots M + N - k) \to n \in ℕ_{0}$
34	6	adantr	$⊢ (φ \land z \in ℂ) \to B : ℕ_{0} ⟶ ℂ$
35	34	ffvelrnda	$⊢ ((φ \land z \in ℂ) \land n \in ℕ_{0}) \to B (n) \in ℂ$
36		expcl	$⊢ (z \in ℂ \land n \in ℕ_{0}) \to z^{n} \in ℂ$
37	36	adantll	$⊢ ((φ \land z \in ℂ) \land n \in ℕ_{0}) \to z^{n} \in ℂ$
38	35 37	mulcld	$⊢ ((φ \land z \in ℂ) \land n \in ℕ_{0}) \to B (n) z^{n} \in ℂ$
39	33 38	sylan2	$⊢ ((φ \land z \in ℂ) \land n \in (0 \dots M + N - k)) \to B (n) z^{n} \in ℂ$
40	32 39	anim12dan	$⊢ ((φ \land z \in ℂ) \land (k \in (0 \dots M + N) \land n \in (0 \dots M + N - k))) \to (A (k) z^{k} \in ℂ \land B (n) z^{n} \in ℂ)$
41		mulcl	$⊢ (A (k) z^{k} \in ℂ \land B (n) z^{n} \in ℂ) \to A (k) z^{k} B (n) z^{n} \in ℂ$
42	40 41	syl	$⊢ ((φ \land z \in ℂ) \land (k \in (0 \dots M + N) \land n \in (0 \dots M + N - k))) \to A (k) z^{k} B (n) z^{n} \in ℂ$
43	21 25 42	fsum0diag2	$⊢ (φ \land z \in ℂ) \to \sum_{k = 0}^{M + N} \sum_{n = 0}^{M + N - k} A (k) z^{k} B (n) z^{n} = \sum_{n = 0}^{M + N} \sum_{k = 0}^{n} A (k) z^{k} B (n - k) z^{n - k}$
44	3	nn0cnd	$⊢ φ \to M \in ℂ$
45	44	ad2antrr	$⊢ ((φ \land z \in ℂ) \land k \in (0 \dots M)) \to M \in ℂ$
46	4	nn0cnd	$⊢ φ \to N \in ℂ$
47	46	ad2antrr	$⊢ ((φ \land z \in ℂ) \land k \in (0 \dots M)) \to N \in ℂ$
48		elfznn0	$⊢ k \in (0 \dots M) \to k \in ℕ_{0}$
49	48	adantl	$⊢ ((φ \land z \in ℂ) \land k \in (0 \dots M)) \to k \in ℕ_{0}$
50	49	nn0cnd	$⊢ ((φ \land z \in ℂ) \land k \in (0 \dots M)) \to k \in ℂ$
51	45 47 50	addsubd	$⊢ ((φ \land z \in ℂ) \land k \in (0 \dots M)) \to M + N - k = M - k + N$
52		fznn0sub	$⊢ k \in (0 \dots M) \to M - k \in ℕ_{0}$
53	52	adantl	$⊢ ((φ \land z \in ℂ) \land k \in (0 \dots M)) \to M - k \in ℕ_{0}$
54		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
55	53 54	eleqtrdi	$⊢ ((φ \land z \in ℂ) \land k \in (0 \dots M)) \to M - k \in ℤ_{\geq 0}$
56	4	nn0zd	$⊢ φ \to N \in ℤ$
57	56	ad2antrr	$⊢ ((φ \land z \in ℂ) \land k \in (0 \dots M)) \to N \in ℤ$
58		eluzadd	$⊢ (M - k \in ℤ_{\geq 0} \land N \in ℤ) \to M - k + N \in ℤ_{\geq (0 + N)}$
59	55 57 58	syl2anc	$⊢ ((φ \land z \in ℂ) \land k \in (0 \dots M)) \to M - k + N \in ℤ_{\geq (0 + N)}$
60	51 59	eqeltrd	$⊢ ((φ \land z \in ℂ) \land k \in (0 \dots M)) \to M + N - k \in ℤ_{\geq (0 + N)}$
61	47	addid2d	$⊢ ((φ \land z \in ℂ) \land k \in (0 \dots M)) \to 0 + N = N$
62	61	fveq2d	$⊢ ((φ \land z \in ℂ) \land k \in (0 \dots M)) \to ℤ_{\geq (0 + N)} = ℤ_{\geq N}$
63	60 62	eleqtrd	$⊢ ((φ \land z \in ℂ) \land k \in (0 \dots M)) \to M + N - k \in ℤ_{\geq N}$
64		fzss2	$⊢ M + N - k \in ℤ_{\geq N} \to (0 \dots N) \subseteq (0 \dots M + N - k)$
65	63 64	syl	$⊢ ((φ \land z \in ℂ) \land k \in (0 \dots M)) \to (0 \dots N) \subseteq (0 \dots M + N - k)$
66	48 31	sylan2	$⊢ ((φ \land z \in ℂ) \land k \in (0 \dots M)) \to A (k) z^{k} \in ℂ$
67	66	adantr	$⊢ (((φ \land z \in ℂ) \land k \in (0 \dots M)) \land n \in (0 \dots N)) \to A (k) z^{k} \in ℂ$
68		elfznn0	$⊢ n \in (0 \dots N) \to n \in ℕ_{0}$
69	68 38	sylan2	$⊢ ((φ \land z \in ℂ) \land n \in (0 \dots N)) \to B (n) z^{n} \in ℂ$
70	69	adantlr	$⊢ (((φ \land z \in ℂ) \land k \in (0 \dots M)) \land n \in (0 \dots N)) \to B (n) z^{n} \in ℂ$
71	67 70	mulcld	$⊢ (((φ \land z \in ℂ) \land k \in (0 \dots M)) \land n \in (0 \dots N)) \to A (k) z^{k} B (n) z^{n} \in ℂ$
72		eldifn	$⊢ n \in ((0 \dots M + N - k) ∖ (0 \dots N)) \to \neg n \in (0 \dots N)$
73	72	adantl	$⊢ (((φ \land z \in ℂ) \land k \in (0 \dots M)) \land n \in ((0 \dots M + N - k) ∖ (0 \dots N))) \to \neg n \in (0 \dots N)$
74		eldifi	$⊢ n \in ((0 \dots M + N - k) ∖ (0 \dots N)) \to n \in (0 \dots M + N - k)$
75	74 33	syl	$⊢ n \in ((0 \dots M + N - k) ∖ (0 \dots N)) \to n \in ℕ_{0}$
76	75	adantl	$⊢ (((φ \land z \in ℂ) \land k \in (0 \dots M)) \land n \in ((0 \dots M + N - k) ∖ (0 \dots N))) \to n \in ℕ_{0}$
77		peano2nn0	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ_{0}$
78	4 77	syl	$⊢ φ \to N + 1 \in ℕ_{0}$
79	78 54	eleqtrdi	$⊢ φ \to N + 1 \in ℤ_{\geq 0}$
80		uzsplit	$⊢ N + 1 \in ℤ_{\geq 0} \to ℤ_{\geq 0} = (0 \dots N + 1 - 1) \cup ℤ_{\geq (N + 1)}$
81	79 80	syl	$⊢ φ \to ℤ_{\geq 0} = (0 \dots N + 1 - 1) \cup ℤ_{\geq (N + 1)}$
82	54 81	eqtrid	$⊢ φ \to ℕ_{0} = (0 \dots N + 1 - 1) \cup ℤ_{\geq (N + 1)}$
83		ax-1cn	$⊢ 1 \in ℂ$
84		pncan	$⊢ (N \in ℂ \land 1 \in ℂ) \to N + 1 - 1 = N$
85	46 83 84	sylancl	$⊢ φ \to N + 1 - 1 = N$
86	85	oveq2d	$⊢ φ \to (0 \dots N + 1 - 1) = (0 \dots N)$
87	86	uneq1d	$⊢ φ \to (0 \dots N + 1 - 1) \cup ℤ_{\geq (N + 1)} = (0 \dots N) \cup ℤ_{\geq (N + 1)}$
88	82 87	eqtrd	$⊢ φ \to ℕ_{0} = (0 \dots N) \cup ℤ_{\geq (N + 1)}$
89	88	ad3antrrr	$⊢ (((φ \land z \in ℂ) \land k \in (0 \dots M)) \land n \in ((0 \dots M + N - k) ∖ (0 \dots N))) \to ℕ_{0} = (0 \dots N) \cup ℤ_{\geq (N + 1)}$
90	76 89	eleqtrd	$⊢ (((φ \land z \in ℂ) \land k \in (0 \dots M)) \land n \in ((0 \dots M + N - k) ∖ (0 \dots N))) \to n \in ((0 \dots N) \cup ℤ_{\geq (N + 1)})$
91		elun	$⊢ n \in ((0 \dots N) \cup ℤ_{\geq (N + 1)}) \leftrightarrow (n \in (0 \dots N) \lor n \in ℤ_{\geq (N + 1)})$
92	90 91	sylib	$⊢ (((φ \land z \in ℂ) \land k \in (0 \dots M)) \land n \in ((0 \dots M + N - k) ∖ (0 \dots N))) \to (n \in (0 \dots N) \lor n \in ℤ_{\geq (N + 1)})$
93	92	ord	$⊢ (((φ \land z \in ℂ) \land k \in (0 \dots M)) \land n \in ((0 \dots M + N - k) ∖ (0 \dots N))) \to (\neg n \in (0 \dots N) \to n \in ℤ_{\geq (N + 1)})$
94	73 93	mpd	$⊢ (((φ \land z \in ℂ) \land k \in (0 \dots M)) \land n \in ((0 \dots M + N - k) ∖ (0 \dots N))) \to n \in ℤ_{\geq (N + 1)}$
95	6	ffund	$⊢ φ \to Fun B$
96		ssun2	$⊢ ℤ_{\geq (N + 1)} \subseteq (0 \dots N + 1 - 1) \cup ℤ_{\geq (N + 1)}$
97	96 82	sseqtrrid	$⊢ φ \to ℤ_{\geq (N + 1)} \subseteq ℕ_{0}$
98	6	fdmd	$⊢ φ \to dom B = ℕ_{0}$
99	97 98	sseqtrrd	$⊢ φ \to ℤ_{\geq (N + 1)} \subseteq dom B$
100		funfvima2	$⊢ (Fun B \land ℤ_{\geq (N + 1)} \subseteq dom B) \to (n \in ℤ_{\geq (N + 1)} \to B (n) \in B [ℤ_{\geq (N + 1)}])$
101	95 99 100	syl2anc	$⊢ φ \to (n \in ℤ_{\geq (N + 1)} \to B (n) \in B [ℤ_{\geq (N + 1)}])$
102	101	ad3antrrr	$⊢ (((φ \land z \in ℂ) \land k \in (0 \dots M)) \land n \in ((0 \dots M + N - k) ∖ (0 \dots N))) \to (n \in ℤ_{\geq (N + 1)} \to B (n) \in B [ℤ_{\geq (N + 1)}])$
103	94 102	mpd	$⊢ (((φ \land z \in ℂ) \land k \in (0 \dots M)) \land n \in ((0 \dots M + N - k) ∖ (0 \dots N))) \to B (n) \in B [ℤ_{\geq (N + 1)}]$
104	8	ad3antrrr	$⊢ (((φ \land z \in ℂ) \land k \in (0 \dots M)) \land n \in ((0 \dots M + N - k) ∖ (0 \dots N))) \to B [ℤ_{\geq (N + 1)}] = \{0\}$
105	103 104	eleqtrd	$⊢ (((φ \land z \in ℂ) \land k \in (0 \dots M)) \land n \in ((0 \dots M + N - k) ∖ (0 \dots N))) \to B (n) \in \{0\}$
106		elsni	$⊢ B (n) \in \{0\} \to B (n) = 0$
107	105 106	syl	$⊢ (((φ \land z \in ℂ) \land k \in (0 \dots M)) \land n \in ((0 \dots M + N - k) ∖ (0 \dots N))) \to B (n) = 0$
108	107	oveq1d	$⊢ (((φ \land z \in ℂ) \land k \in (0 \dots M)) \land n \in ((0 \dots M + N - k) ∖ (0 \dots N))) \to B (n) z^{n} = 0 \cdot z^{n}$
109		simplr	$⊢ ((φ \land z \in ℂ) \land k \in (0 \dots M)) \to z \in ℂ$
110	109 75 36	syl2an	$⊢ (((φ \land z \in ℂ) \land k \in (0 \dots M)) \land n \in ((0 \dots M + N - k) ∖ (0 \dots N))) \to z^{n} \in ℂ$
111	110	mul02d	$⊢ (((φ \land z \in ℂ) \land k \in (0 \dots M)) \land n \in ((0 \dots M + N - k) ∖ (0 \dots N))) \to 0 \cdot z^{n} = 0$
112	108 111	eqtrd	$⊢ (((φ \land z \in ℂ) \land k \in (0 \dots M)) \land n \in ((0 \dots M + N - k) ∖ (0 \dots N))) \to B (n) z^{n} = 0$
113	112	oveq2d	$⊢ (((φ \land z \in ℂ) \land k \in (0 \dots M)) \land n \in ((0 \dots M + N - k) ∖ (0 \dots N))) \to A (k) z^{k} B (n) z^{n} = A (k) z^{k} \cdot 0$
114	66	adantr	$⊢ (((φ \land z \in ℂ) \land k \in (0 \dots M)) \land n \in ((0 \dots M + N - k) ∖ (0 \dots N))) \to A (k) z^{k} \in ℂ$
115	114	mul01d	$⊢ (((φ \land z \in ℂ) \land k \in (0 \dots M)) \land n \in ((0 \dots M + N - k) ∖ (0 \dots N))) \to A (k) z^{k} \cdot 0 = 0$
116	113 115	eqtrd	$⊢ (((φ \land z \in ℂ) \land k \in (0 \dots M)) \land n \in ((0 \dots M + N - k) ∖ (0 \dots N))) \to A (k) z^{k} B (n) z^{n} = 0$
117		fzfid	$⊢ ((φ \land z \in ℂ) \land k \in (0 \dots M)) \to (0 \dots M + N - k) \in Fin$
118	65 71 116 117	fsumss	$⊢ ((φ \land z \in ℂ) \land k \in (0 \dots M)) \to \sum_{n = 0}^{N} A (k) z^{k} B (n) z^{n} = \sum_{n = 0}^{M + N - k} A (k) z^{k} B (n) z^{n}$
119	118	sumeq2dv	$⊢ (φ \land z \in ℂ) \to \sum_{k = 0}^{M} \sum_{n = 0}^{N} A (k) z^{k} B (n) z^{n} = \sum_{k = 0}^{M} \sum_{n = 0}^{M + N - k} A (k) z^{k} B (n) z^{n}$
120		fzfid	$⊢ (φ \land z \in ℂ) \to (0 \dots M) \in Fin$
121		fzfid	$⊢ (φ \land z \in ℂ) \to (0 \dots N) \in Fin$
122	120 121 66 69	fsum2mul	$⊢ (φ \land z \in ℂ) \to \sum_{k = 0}^{M} \sum_{n = 0}^{N} A (k) z^{k} B (n) z^{n} = \sum_{k = 0}^{M} A (k) z^{k} \sum_{n = 0}^{N} B (n) z^{n}$
123	44 46	addcomd	$⊢ φ \to M + N = N + M$
124	4 54	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 0}$
125	3	nn0zd	$⊢ φ \to M \in ℤ$
126		eluzadd	$⊢ (N \in ℤ_{\geq 0} \land M \in ℤ) \to N + M \in ℤ_{\geq (0 + M)}$
127	124 125 126	syl2anc	$⊢ φ \to N + M \in ℤ_{\geq (0 + M)}$
128	44	addid2d	$⊢ φ \to 0 + M = M$
129	128	fveq2d	$⊢ φ \to ℤ_{\geq (0 + M)} = ℤ_{\geq M}$
130	127 129	eleqtrd	$⊢ φ \to N + M \in ℤ_{\geq M}$
131	123 130	eqeltrd	$⊢ φ \to M + N \in ℤ_{\geq M}$
132		fzss2	$⊢ M + N \in ℤ_{\geq M} \to (0 \dots M) \subseteq (0 \dots M + N)$
133	131 132	syl	$⊢ φ \to (0 \dots M) \subseteq (0 \dots M + N)$
134	133	adantr	$⊢ (φ \land z \in ℂ) \to (0 \dots M) \subseteq (0 \dots M + N)$
135	66	adantr	$⊢ (((φ \land z \in ℂ) \land k \in (0 \dots M)) \land n \in (0 \dots M + N - k)) \to A (k) z^{k} \in ℂ$
136	39	adantlr	$⊢ (((φ \land z \in ℂ) \land k \in (0 \dots M)) \land n \in (0 \dots M + N - k)) \to B (n) z^{n} \in ℂ$
137	135 136	mulcld	$⊢ (((φ \land z \in ℂ) \land k \in (0 \dots M)) \land n \in (0 \dots M + N - k)) \to A (k) z^{k} B (n) z^{n} \in ℂ$
138	117 137	fsumcl	$⊢ ((φ \land z \in ℂ) \land k \in (0 \dots M)) \to \sum_{n = 0}^{M + N - k} A (k) z^{k} B (n) z^{n} \in ℂ$
139		eldifn	$⊢ k \in ((0 \dots M + N) ∖ (0 \dots M)) \to \neg k \in (0 \dots M)$
140	139	adantl	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots M))) \to \neg k \in (0 \dots M)$
141		eldifi	$⊢ k \in ((0 \dots M + N) ∖ (0 \dots M)) \to k \in (0 \dots M + N)$
142	141 26	syl	$⊢ k \in ((0 \dots M + N) ∖ (0 \dots M)) \to k \in ℕ_{0}$
143	142	adantl	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots M))) \to k \in ℕ_{0}$
144		peano2nn0	$⊢ M \in ℕ_{0} \to M + 1 \in ℕ_{0}$
145	3 144	syl	$⊢ φ \to M + 1 \in ℕ_{0}$
146	145 54	eleqtrdi	$⊢ φ \to M + 1 \in ℤ_{\geq 0}$
147		uzsplit	$⊢ M + 1 \in ℤ_{\geq 0} \to ℤ_{\geq 0} = (0 \dots M + 1 - 1) \cup ℤ_{\geq (M + 1)}$
148	146 147	syl	$⊢ φ \to ℤ_{\geq 0} = (0 \dots M + 1 - 1) \cup ℤ_{\geq (M + 1)}$
149	54 148	eqtrid	$⊢ φ \to ℕ_{0} = (0 \dots M + 1 - 1) \cup ℤ_{\geq (M + 1)}$
150		pncan	$⊢ (M \in ℂ \land 1 \in ℂ) \to M + 1 - 1 = M$
151	44 83 150	sylancl	$⊢ φ \to M + 1 - 1 = M$
152	151	oveq2d	$⊢ φ \to (0 \dots M + 1 - 1) = (0 \dots M)$
153	152	uneq1d	$⊢ φ \to (0 \dots M + 1 - 1) \cup ℤ_{\geq (M + 1)} = (0 \dots M) \cup ℤ_{\geq (M + 1)}$
154	149 153	eqtrd	$⊢ φ \to ℕ_{0} = (0 \dots M) \cup ℤ_{\geq (M + 1)}$
155	154	ad2antrr	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots M))) \to ℕ_{0} = (0 \dots M) \cup ℤ_{\geq (M + 1)}$
156	143 155	eleqtrd	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots M))) \to k \in ((0 \dots M) \cup ℤ_{\geq (M + 1)})$
157		elun	$⊢ k \in ((0 \dots M) \cup ℤ_{\geq (M + 1)}) \leftrightarrow (k \in (0 \dots M) \lor k \in ℤ_{\geq (M + 1)})$
158	156 157	sylib	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots M))) \to (k \in (0 \dots M) \lor k \in ℤ_{\geq (M + 1)})$
159	158	ord	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots M))) \to (\neg k \in (0 \dots M) \to k \in ℤ_{\geq (M + 1)})$
160	140 159	mpd	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots M))) \to k \in ℤ_{\geq (M + 1)}$
161	5	ffund	$⊢ φ \to Fun A$
162		ssun2	$⊢ ℤ_{\geq (M + 1)} \subseteq (0 \dots M + 1 - 1) \cup ℤ_{\geq (M + 1)}$
163	162 149	sseqtrrid	$⊢ φ \to ℤ_{\geq (M + 1)} \subseteq ℕ_{0}$
164	5	fdmd	$⊢ φ \to dom A = ℕ_{0}$
165	163 164	sseqtrrd	$⊢ φ \to ℤ_{\geq (M + 1)} \subseteq dom A$
166		funfvima2	$⊢ (Fun A \land ℤ_{\geq (M + 1)} \subseteq dom A) \to (k \in ℤ_{\geq (M + 1)} \to A (k) \in A [ℤ_{\geq (M + 1)}])$
167	161 165 166	syl2anc	$⊢ φ \to (k \in ℤ_{\geq (M + 1)} \to A (k) \in A [ℤ_{\geq (M + 1)}])$
168	167	ad2antrr	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots M))) \to (k \in ℤ_{\geq (M + 1)} \to A (k) \in A [ℤ_{\geq (M + 1)}])$
169	160 168	mpd	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots M))) \to A (k) \in A [ℤ_{\geq (M + 1)}]$
170	7	ad2antrr	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots M))) \to A [ℤ_{\geq (M + 1)}] = \{0\}$
171	169 170	eleqtrd	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots M))) \to A (k) \in \{0\}$
172		elsni	$⊢ A (k) \in \{0\} \to A (k) = 0$
173	171 172	syl	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots M))) \to A (k) = 0$
174	173	oveq1d	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots M))) \to A (k) z^{k} = 0 \cdot z^{k}$
175	142 30	sylan2	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots M))) \to z^{k} \in ℂ$
176	175	mul02d	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots M))) \to 0 \cdot z^{k} = 0$
177	174 176	eqtrd	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots M))) \to A (k) z^{k} = 0$
178	177	adantr	$⊢ (((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots M))) \land n \in (0 \dots M + N - k)) \to A (k) z^{k} = 0$
179	178	oveq1d	$⊢ (((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots M))) \land n \in (0 \dots M + N - k)) \to A (k) z^{k} B (n) z^{n} = 0 \cdot B (n) z^{n}$
180	39	adantlr	$⊢ (((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots M))) \land n \in (0 \dots M + N - k)) \to B (n) z^{n} \in ℂ$
181	180	mul02d	$⊢ (((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots M))) \land n \in (0 \dots M + N - k)) \to 0 \cdot B (n) z^{n} = 0$
182	179 181	eqtrd	$⊢ (((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots M))) \land n \in (0 \dots M + N - k)) \to A (k) z^{k} B (n) z^{n} = 0$
183	182	sumeq2dv	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots M))) \to \sum_{n = 0}^{M + N - k} A (k) z^{k} B (n) z^{n} = \sum_{n = 0}^{M + N - k} 0$
184		fzfid	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots M))) \to (0 \dots M + N - k) \in Fin$
185	184	olcd	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots M))) \to ((0 \dots M + N - k) \subseteq ℤ_{\geq 0} \lor (0 \dots M + N - k) \in Fin)$
186		sumz	$⊢ ((0 \dots M + N - k) \subseteq ℤ_{\geq 0} \lor (0 \dots M + N - k) \in Fin) \to \sum_{n = 0}^{M + N - k} 0 = 0$
187	185 186	syl	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots M))) \to \sum_{n = 0}^{M + N - k} 0 = 0$
188	183 187	eqtrd	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots M))) \to \sum_{n = 0}^{M + N - k} A (k) z^{k} B (n) z^{n} = 0$
189		fzfid	$⊢ (φ \land z \in ℂ) \to (0 \dots M + N) \in Fin$
190	134 138 188 189	fsumss	$⊢ (φ \land z \in ℂ) \to \sum_{k = 0}^{M} \sum_{n = 0}^{M + N - k} A (k) z^{k} B (n) z^{n} = \sum_{k = 0}^{M + N} \sum_{n = 0}^{M + N - k} A (k) z^{k} B (n) z^{n}$
191	119 122 190	3eqtr3d	$⊢ (φ \land z \in ℂ) \to \sum_{k = 0}^{M} A (k) z^{k} \sum_{n = 0}^{N} B (n) z^{n} = \sum_{k = 0}^{M + N} \sum_{n = 0}^{M + N - k} A (k) z^{k} B (n) z^{n}$
192		fzfid	$⊢ ((φ \land z \in ℂ) \land n \in (0 \dots M + N)) \to (0 \dots n) \in Fin$
193		elfznn0	$⊢ n \in (0 \dots M + N) \to n \in ℕ_{0}$
194	193 37	sylan2	$⊢ ((φ \land z \in ℂ) \land n \in (0 \dots M + N)) \to z^{n} \in ℂ$
195		simpll	$⊢ ((φ \land z \in ℂ) \land n \in (0 \dots M + N)) \to φ$
196		elfznn0	$⊢ k \in (0 \dots n) \to k \in ℕ_{0}$
197	5	ffvelrnda	$⊢ (φ \land k \in ℕ_{0}) \to A (k) \in ℂ$
198	195 196 197	syl2an	$⊢ (((φ \land z \in ℂ) \land n \in (0 \dots M + N)) \land k \in (0 \dots n)) \to A (k) \in ℂ$
199		fznn0sub	$⊢ k \in (0 \dots n) \to n - k \in ℕ_{0}$
200	6	ffvelrnda	$⊢ (φ \land n - k \in ℕ_{0}) \to B (n - k) \in ℂ$
201	195 199 200	syl2an	$⊢ (((φ \land z \in ℂ) \land n \in (0 \dots M + N)) \land k \in (0 \dots n)) \to B (n - k) \in ℂ$
202	198 201	mulcld	$⊢ (((φ \land z \in ℂ) \land n \in (0 \dots M + N)) \land k \in (0 \dots n)) \to A (k) B (n - k) \in ℂ$
203	192 194 202	fsummulc1	$⊢ ((φ \land z \in ℂ) \land n \in (0 \dots M + N)) \to \sum_{k = 0}^{n} A (k) B (n - k) z^{n} = \sum_{k = 0}^{n} A (k) B (n - k) z^{n}$
204		simplr	$⊢ ((φ \land z \in ℂ) \land n \in (0 \dots M + N)) \to z \in ℂ$
205	204 196 29	syl2an	$⊢ (((φ \land z \in ℂ) \land n \in (0 \dots M + N)) \land k \in (0 \dots n)) \to z^{k} \in ℂ$
206		expcl	$⊢ (z \in ℂ \land n - k \in ℕ_{0}) \to z^{n - k} \in ℂ$
207	204 199 206	syl2an	$⊢ (((φ \land z \in ℂ) \land n \in (0 \dots M + N)) \land k \in (0 \dots n)) \to z^{n - k} \in ℂ$
208	198 205 201 207	mul4d	$⊢ (((φ \land z \in ℂ) \land n \in (0 \dots M + N)) \land k \in (0 \dots n)) \to A (k) z^{k} B (n - k) z^{n - k} = A (k) B (n - k) z^{k} z^{n - k}$
209	204	adantr	$⊢ (((φ \land z \in ℂ) \land n \in (0 \dots M + N)) \land k \in (0 \dots n)) \to z \in ℂ$
210	199	adantl	$⊢ (((φ \land z \in ℂ) \land n \in (0 \dots M + N)) \land k \in (0 \dots n)) \to n - k \in ℕ_{0}$
211	196	adantl	$⊢ (((φ \land z \in ℂ) \land n \in (0 \dots M + N)) \land k \in (0 \dots n)) \to k \in ℕ_{0}$
212	209 210 211	expaddd	$⊢ (((φ \land z \in ℂ) \land n \in (0 \dots M + N)) \land k \in (0 \dots n)) \to z^{k + n - k} = z^{k} z^{n - k}$
213	211	nn0cnd	$⊢ (((φ \land z \in ℂ) \land n \in (0 \dots M + N)) \land k \in (0 \dots n)) \to k \in ℂ$
214	193	ad2antlr	$⊢ (((φ \land z \in ℂ) \land n \in (0 \dots M + N)) \land k \in (0 \dots n)) \to n \in ℕ_{0}$
215	214	nn0cnd	$⊢ (((φ \land z \in ℂ) \land n \in (0 \dots M + N)) \land k \in (0 \dots n)) \to n \in ℂ$
216	213 215	pncan3d	$⊢ (((φ \land z \in ℂ) \land n \in (0 \dots M + N)) \land k \in (0 \dots n)) \to k + n - k = n$
217	216	oveq2d	$⊢ (((φ \land z \in ℂ) \land n \in (0 \dots M + N)) \land k \in (0 \dots n)) \to z^{k + n - k} = z^{n}$
218	212 217	eqtr3d	$⊢ (((φ \land z \in ℂ) \land n \in (0 \dots M + N)) \land k \in (0 \dots n)) \to z^{k} z^{n - k} = z^{n}$
219	218	oveq2d	$⊢ (((φ \land z \in ℂ) \land n \in (0 \dots M + N)) \land k \in (0 \dots n)) \to A (k) B (n - k) z^{k} z^{n - k} = A (k) B (n - k) z^{n}$
220	208 219	eqtrd	$⊢ (((φ \land z \in ℂ) \land n \in (0 \dots M + N)) \land k \in (0 \dots n)) \to A (k) z^{k} B (n - k) z^{n - k} = A (k) B (n - k) z^{n}$
221	220	sumeq2dv	$⊢ ((φ \land z \in ℂ) \land n \in (0 \dots M + N)) \to \sum_{k = 0}^{n} A (k) z^{k} B (n - k) z^{n - k} = \sum_{k = 0}^{n} A (k) B (n - k) z^{n}$
222	203 221	eqtr4d	$⊢ ((φ \land z \in ℂ) \land n \in (0 \dots M + N)) \to \sum_{k = 0}^{n} A (k) B (n - k) z^{n} = \sum_{k = 0}^{n} A (k) z^{k} B (n - k) z^{n - k}$
223	222	sumeq2dv	$⊢ (φ \land z \in ℂ) \to \sum_{n = 0}^{M + N} \sum_{k = 0}^{n} A (k) B (n - k) z^{n} = \sum_{n = 0}^{M + N} \sum_{k = 0}^{n} A (k) z^{k} B (n - k) z^{n - k}$
224	43 191 223	3eqtr4rd	$⊢ (φ \land z \in ℂ) \to \sum_{n = 0}^{M + N} \sum_{k = 0}^{n} A (k) B (n - k) z^{n} = \sum_{k = 0}^{M} A (k) z^{k} \sum_{n = 0}^{N} B (n) z^{n}$
225		fveq2	$⊢ n = k \to B (n) = B (k)$
226		oveq2	$⊢ n = k \to z^{n} = z^{k}$
227	225 226	oveq12d	$⊢ n = k \to B (n) z^{n} = B (k) z^{k}$
228	227	cbvsumv	$⊢ \sum_{n = 0}^{N} B (n) z^{n} = \sum_{k = 0}^{N} B (k) z^{k}$
229	228	oveq2i	$⊢ \sum_{k = 0}^{M} A (k) z^{k} \sum_{n = 0}^{N} B (n) z^{n} = \sum_{k = 0}^{M} A (k) z^{k} \sum_{k = 0}^{N} B (k) z^{k}$
230	224 229	eqtrdi	$⊢ (φ \land z \in ℂ) \to \sum_{n = 0}^{M + N} \sum_{k = 0}^{n} A (k) B (n - k) z^{n} = \sum_{k = 0}^{M} A (k) z^{k} \sum_{k = 0}^{N} B (k) z^{k}$
231	230	mpteq2dva	$⊢ φ \to (z \in ℂ ⟼ \sum_{n = 0}^{M + N} \sum_{k = 0}^{n} A (k) B (n - k) z^{n}) = (z \in ℂ ⟼ \sum_{k = 0}^{M} A (k) z^{k} \sum_{k = 0}^{N} B (k) z^{k})$
232	17 231	eqtr4d	$⊢ φ \to F \times_{f} G = (z \in ℂ ⟼ \sum_{n = 0}^{M + N} \sum_{k = 0}^{n} A (k) B (n - k) z^{n})$

Metamath Proof Explorer

Theorem plymullem1

Proof