coemullem

	Ref	Expression
Hypotheses	coefv0.1	$⊢ A = coeff (F)$
	coeadd.2	$⊢ B = coeff (G)$
	coeadd.3	$⊢ M = \deg (F)$
	coeadd.4	$⊢ N = \deg (G)$
Assertion	coemullem	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to (coeff (F \times_{f} G) = (n \in ℕ_{0} ⟼ \sum_{k = 0}^{n} A (k) B (n - k)) \land \deg (F \times_{f} G) \leq M + N)$

Proof

Step	Hyp	Ref	Expression
1		coefv0.1	$⊢ A = coeff (F)$
2		coeadd.2	$⊢ B = coeff (G)$
3		coeadd.3	$⊢ M = \deg (F)$
4		coeadd.4	$⊢ N = \deg (G)$
5		plymulcl	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to F \times_{f} G \in Poly (ℂ)$
6		dgrcl	$⊢ F \in Poly (S) \to \deg (F) \in ℕ_{0}$
7	3 6	eqeltrid	$⊢ F \in Poly (S) \to M \in ℕ_{0}$
8		dgrcl	$⊢ G \in Poly (S) \to \deg (G) \in ℕ_{0}$
9	4 8	eqeltrid	$⊢ G \in Poly (S) \to N \in ℕ_{0}$
10		nn0addcl	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to M + N \in ℕ_{0}$
11	7 9 10	syl2an	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to M + N \in ℕ_{0}$
12		fzfid	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land n \in ℕ_{0}) \to (0 \dots n) \in Fin$
13	1	coef3	$⊢ F \in Poly (S) \to A : ℕ_{0} ⟶ ℂ$
14	13	adantr	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to A : ℕ_{0} ⟶ ℂ$
15	14	adantr	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land n \in ℕ_{0}) \to A : ℕ_{0} ⟶ ℂ$
16		elfznn0	$⊢ k \in (0 \dots n) \to k \in ℕ_{0}$
17		ffvelcdm	$⊢ (A : ℕ_{0} ⟶ ℂ \land k \in ℕ_{0}) \to A (k) \in ℂ$
18	15 16 17	syl2an	$⊢ (((F \in Poly (S) \land G \in Poly (S)) \land n \in ℕ_{0}) \land k \in (0 \dots n)) \to A (k) \in ℂ$
19	2	coef3	$⊢ G \in Poly (S) \to B : ℕ_{0} ⟶ ℂ$
20	19	adantl	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to B : ℕ_{0} ⟶ ℂ$
21	20	ad2antrr	$⊢ (((F \in Poly (S) \land G \in Poly (S)) \land n \in ℕ_{0}) \land k \in (0 \dots n)) \to B : ℕ_{0} ⟶ ℂ$
22		fznn0sub	$⊢ k \in (0 \dots n) \to n - k \in ℕ_{0}$
23	22	adantl	$⊢ (((F \in Poly (S) \land G \in Poly (S)) \land n \in ℕ_{0}) \land k \in (0 \dots n)) \to n - k \in ℕ_{0}$
24	21 23	ffvelcdmd	$⊢ (((F \in Poly (S) \land G \in Poly (S)) \land n \in ℕ_{0}) \land k \in (0 \dots n)) \to B (n - k) \in ℂ$
25	18 24	mulcld	$⊢ (((F \in Poly (S) \land G \in Poly (S)) \land n \in ℕ_{0}) \land k \in (0 \dots n)) \to A (k) B (n - k) \in ℂ$
26	12 25	fsumcl	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land n \in ℕ_{0}) \to \sum_{k = 0}^{n} A (k) B (n - k) \in ℂ$
27	26	fmpttd	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to (n \in ℕ_{0} ⟼ \sum_{k = 0}^{n} A (k) B (n - k)) : ℕ_{0} ⟶ ℂ$
28		oveq2	$⊢ n = j \to (0 \dots n) = (0 \dots j)$
29		fvoveq1	$⊢ n = j \to B (n - k) = B (j - k)$
30	29	oveq2d	$⊢ n = j \to A (k) B (n - k) = A (k) B (j - k)$
31	30	adantr	$⊢ (n = j \land k \in (0 \dots n)) \to A (k) B (n - k) = A (k) B (j - k)$
32	28 31	sumeq12dv	$⊢ n = j \to \sum_{k = 0}^{n} A (k) B (n - k) = \sum_{k = 0}^{j} A (k) B (j - k)$
33		eqid	$⊢ (n \in ℕ_{0} ⟼ \sum_{k = 0}^{n} A (k) B (n - k)) = (n \in ℕ_{0} ⟼ \sum_{k = 0}^{n} A (k) B (n - k))$
34		sumex	$⊢ \sum_{k = 0}^{j} A (k) B (j - k) \in V$
35	32 33 34	fvmpt	$⊢ j \in ℕ_{0} \to (n \in ℕ_{0} ⟼ \sum_{k = 0}^{n} A (k) B (n - k)) (j) = \sum_{k = 0}^{j} A (k) B (j - k)$
36	35	ad2antrl	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N)) \to (n \in ℕ_{0} ⟼ \sum_{k = 0}^{n} A (k) B (n - k)) (j) = \sum_{k = 0}^{j} A (k) B (j - k)$
37		simp2r	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N) \land (k \in (0 \dots j) \land k \leq M)) \to \neg j \leq M + N$
38		simp2l	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N) \land (k \in (0 \dots j) \land k \leq M)) \to j \in ℕ_{0}$
39	38	nn0red	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N) \land (k \in (0 \dots j) \land k \leq M)) \to j \in ℝ$
40		simp3l	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N) \land (k \in (0 \dots j) \land k \leq M)) \to k \in (0 \dots j)$
41		elfznn0	$⊢ k \in (0 \dots j) \to k \in ℕ_{0}$
42	40 41	syl	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N) \land (k \in (0 \dots j) \land k \leq M)) \to k \in ℕ_{0}$
43	42	nn0red	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N) \land (k \in (0 \dots j) \land k \leq M)) \to k \in ℝ$
44	9	adantl	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to N \in ℕ_{0}$
45	44	3ad2ant1	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N) \land (k \in (0 \dots j) \land k \leq M)) \to N \in ℕ_{0}$
46	45	nn0red	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N) \land (k \in (0 \dots j) \land k \leq M)) \to N \in ℝ$
47	39 43 46	lesubadd2d	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N) \land (k \in (0 \dots j) \land k \leq M)) \to (j - k \leq N \leftrightarrow j \leq k + N)$
48	7	adantr	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to M \in ℕ_{0}$
49	48	3ad2ant1	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N) \land (k \in (0 \dots j) \land k \leq M)) \to M \in ℕ_{0}$
50	49	nn0red	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N) \land (k \in (0 \dots j) \land k \leq M)) \to M \in ℝ$
51		simp3r	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N) \land (k \in (0 \dots j) \land k \leq M)) \to k \leq M$
52	43 50 46 51	leadd1dd	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N) \land (k \in (0 \dots j) \land k \leq M)) \to k + N \leq M + N$
53	43 46	readdcld	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N) \land (k \in (0 \dots j) \land k \leq M)) \to k + N \in ℝ$
54	50 46	readdcld	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N) \land (k \in (0 \dots j) \land k \leq M)) \to M + N \in ℝ$
55		letr	$⊢ (j \in ℝ \land k + N \in ℝ \land M + N \in ℝ) \to ((j \leq k + N \land k + N \leq M + N) \to j \leq M + N)$
56	39 53 54 55	syl3anc	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N) \land (k \in (0 \dots j) \land k \leq M)) \to ((j \leq k + N \land k + N \leq M + N) \to j \leq M + N)$
57	52 56	mpan2d	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N) \land (k \in (0 \dots j) \land k \leq M)) \to (j \leq k + N \to j \leq M + N)$
58	47 57	sylbid	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N) \land (k \in (0 \dots j) \land k \leq M)) \to (j - k \leq N \to j \leq M + N)$
59	37 58	mtod	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N) \land (k \in (0 \dots j) \land k \leq M)) \to \neg j - k \leq N$
60		simpr	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to G \in Poly (S)$
61	60	3ad2ant1	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N) \land (k \in (0 \dots j) \land k \leq M)) \to G \in Poly (S)$
62		fznn0sub	$⊢ k \in (0 \dots j) \to j - k \in ℕ_{0}$
63	40 62	syl	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N) \land (k \in (0 \dots j) \land k \leq M)) \to j - k \in ℕ_{0}$
64	2 4	dgrub	$⊢ (G \in Poly (S) \land j - k \in ℕ_{0} \land B (j - k) \neq 0) \to j - k \leq N$
65	64	3expia	$⊢ (G \in Poly (S) \land j - k \in ℕ_{0}) \to (B (j - k) \neq 0 \to j - k \leq N)$
66	61 63 65	syl2anc	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N) \land (k \in (0 \dots j) \land k \leq M)) \to (B (j - k) \neq 0 \to j - k \leq N)$
67	66	necon1bd	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N) \land (k \in (0 \dots j) \land k \leq M)) \to (\neg j - k \leq N \to B (j - k) = 0)$
68	59 67	mpd	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N) \land (k \in (0 \dots j) \land k \leq M)) \to B (j - k) = 0$
69	68	oveq2d	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N) \land (k \in (0 \dots j) \land k \leq M)) \to A (k) B (j - k) = A (k) \cdot 0$
70	14	3ad2ant1	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N) \land (k \in (0 \dots j) \land k \leq M)) \to A : ℕ_{0} ⟶ ℂ$
71	70 42	ffvelcdmd	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N) \land (k \in (0 \dots j) \land k \leq M)) \to A (k) \in ℂ$
72	71	mul01d	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N) \land (k \in (0 \dots j) \land k \leq M)) \to A (k) \cdot 0 = 0$
73	69 72	eqtrd	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N) \land (k \in (0 \dots j) \land k \leq M)) \to A (k) B (j - k) = 0$
74	73	3expia	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N)) \to ((k \in (0 \dots j) \land k \leq M) \to A (k) B (j - k) = 0)$
75	74	impl	$⊢ ((((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N)) \land k \in (0 \dots j)) \land k \leq M) \to A (k) B (j - k) = 0$
76		simpl	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to F \in Poly (S)$
77	76	adantr	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N)) \to F \in Poly (S)$
78	1 3	dgrub	$⊢ (F \in Poly (S) \land k \in ℕ_{0} \land A (k) \neq 0) \to k \leq M$
79	78	3expia	$⊢ (F \in Poly (S) \land k \in ℕ_{0}) \to (A (k) \neq 0 \to k \leq M)$
80	77 41 79	syl2an	$⊢ (((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N)) \land k \in (0 \dots j)) \to (A (k) \neq 0 \to k \leq M)$
81	80	necon1bd	$⊢ (((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N)) \land k \in (0 \dots j)) \to (\neg k \leq M \to A (k) = 0)$
82	81	imp	$⊢ ((((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N)) \land k \in (0 \dots j)) \land \neg k \leq M) \to A (k) = 0$
83	82	oveq1d	$⊢ ((((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N)) \land k \in (0 \dots j)) \land \neg k \leq M) \to A (k) B (j - k) = 0 \cdot B (j - k)$
84	20	ad3antrrr	$⊢ ((((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N)) \land k \in (0 \dots j)) \land \neg k \leq M) \to B : ℕ_{0} ⟶ ℂ$
85	62	ad2antlr	$⊢ ((((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N)) \land k \in (0 \dots j)) \land \neg k \leq M) \to j - k \in ℕ_{0}$
86	84 85	ffvelcdmd	$⊢ ((((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N)) \land k \in (0 \dots j)) \land \neg k \leq M) \to B (j - k) \in ℂ$
87	86	mul02d	$⊢ ((((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N)) \land k \in (0 \dots j)) \land \neg k \leq M) \to 0 \cdot B (j - k) = 0$
88	83 87	eqtrd	$⊢ ((((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N)) \land k \in (0 \dots j)) \land \neg k \leq M) \to A (k) B (j - k) = 0$
89	75 88	pm2.61dan	$⊢ (((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N)) \land k \in (0 \dots j)) \to A (k) B (j - k) = 0$
90	89	sumeq2dv	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N)) \to \sum_{k = 0}^{j} A (k) B (j - k) = \sum_{k = 0}^{j} 0$
91		fzfi	$⊢ (0 \dots j) \in Fin$
92	91	olci	$⊢ ((0 \dots j) \subseteq ℤ_{\geq 0} \lor (0 \dots j) \in Fin)$
93		sumz	$⊢ ((0 \dots j) \subseteq ℤ_{\geq 0} \lor (0 \dots j) \in Fin) \to \sum_{k = 0}^{j} 0 = 0$
94	92 93	ax-mp	$⊢ \sum_{k = 0}^{j} 0 = 0$
95	90 94	eqtrdi	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N)) \to \sum_{k = 0}^{j} A (k) B (j - k) = 0$
96	36 95	eqtrd	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (j \in ℕ_{0} \land \neg j \leq M + N)) \to (n \in ℕ_{0} ⟼ \sum_{k = 0}^{n} A (k) B (n - k)) (j) = 0$
97	96	expr	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land j \in ℕ_{0}) \to (\neg j \leq M + N \to (n \in ℕ_{0} ⟼ \sum_{k = 0}^{n} A (k) B (n - k)) (j) = 0)$
98	97	necon1ad	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land j \in ℕ_{0}) \to ((n \in ℕ_{0} ⟼ \sum_{k = 0}^{n} A (k) B (n - k)) (j) \neq 0 \to j \leq M + N)$
99	98	ralrimiva	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to \forall j \in ℕ_{0} ((n \in ℕ_{0} ⟼ \sum_{k = 0}^{n} A (k) B (n - k)) (j) \neq 0 \to j \leq M + N)$
100		plyco0	$⊢ (M + N \in ℕ_{0} \land (n \in ℕ_{0} ⟼ \sum_{k = 0}^{n} A (k) B (n - k)) : ℕ_{0} ⟶ ℂ) \to ((n \in ℕ_{0} ⟼ \sum_{k = 0}^{n} A (k) B (n - k)) [ℤ_{\geq (M + N + 1)}] = \{0\} \leftrightarrow \forall j \in ℕ_{0} ((n \in ℕ_{0} ⟼ \sum_{k = 0}^{n} A (k) B (n - k)) (j) \neq 0 \to j \leq M + N))$
101	11 27 100	syl2anc	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to ((n \in ℕ_{0} ⟼ \sum_{k = 0}^{n} A (k) B (n - k)) [ℤ_{\geq (M + N + 1)}] = \{0\} \leftrightarrow \forall j \in ℕ_{0} ((n \in ℕ_{0} ⟼ \sum_{k = 0}^{n} A (k) B (n - k)) (j) \neq 0 \to j \leq M + N))$
102	99 101	mpbird	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to (n \in ℕ_{0} ⟼ \sum_{k = 0}^{n} A (k) B (n - k)) [ℤ_{\geq (M + N + 1)}] = \{0\}$
103	1 3	dgrub2	$⊢ F \in Poly (S) \to A [ℤ_{\geq (M + 1)}] = \{0\}$
104	103	adantr	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to A [ℤ_{\geq (M + 1)}] = \{0\}$
105	2 4	dgrub2	$⊢ G \in Poly (S) \to B [ℤ_{\geq (N + 1)}] = \{0\}$
106	105	adantl	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to B [ℤ_{\geq (N + 1)}] = \{0\}$
107	1 3	coeid	$⊢ F \in Poly (S) \to F = (z \in ℂ ⟼ \sum_{k = 0}^{M} A (k) z^{k})$
108	107	adantr	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to F = (z \in ℂ ⟼ \sum_{k = 0}^{M} A (k) z^{k})$
109	2 4	coeid	$⊢ G \in Poly (S) \to G = (z \in ℂ ⟼ \sum_{k = 0}^{N} B (k) z^{k})$
110	109	adantl	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to G = (z \in ℂ ⟼ \sum_{k = 0}^{N} B (k) z^{k})$
111	76 60 48 44 14 20 104 106 108 110	plymullem1	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to F \times_{f} G = (z \in ℂ ⟼ \sum_{j = 0}^{M + N} \sum_{k = 0}^{j} A (k) B (j - k) z^{j})$
112		elfznn0	$⊢ j \in (0 \dots M + N) \to j \in ℕ_{0}$
113	112 35	syl	$⊢ j \in (0 \dots M + N) \to (n \in ℕ_{0} ⟼ \sum_{k = 0}^{n} A (k) B (n - k)) (j) = \sum_{k = 0}^{j} A (k) B (j - k)$
114	113	oveq1d	$⊢ j \in (0 \dots M + N) \to (n \in ℕ_{0} ⟼ \sum_{k = 0}^{n} A (k) B (n - k)) (j) z^{j} = \sum_{k = 0}^{j} A (k) B (j - k) z^{j}$
115	114	sumeq2i	$⊢ \sum_{j = 0}^{M + N} (n \in ℕ_{0} ⟼ \sum_{k = 0}^{n} A (k) B (n - k)) (j) z^{j} = \sum_{j = 0}^{M + N} \sum_{k = 0}^{j} A (k) B (j - k) z^{j}$
116	115	mpteq2i	$⊢ (z \in ℂ ⟼ \sum_{j = 0}^{M + N} (n \in ℕ_{0} ⟼ \sum_{k = 0}^{n} A (k) B (n - k)) (j) z^{j}) = (z \in ℂ ⟼ \sum_{j = 0}^{M + N} \sum_{k = 0}^{j} A (k) B (j - k) z^{j})$
117	111 116	eqtr4di	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to F \times_{f} G = (z \in ℂ ⟼ \sum_{j = 0}^{M + N} (n \in ℕ_{0} ⟼ \sum_{k = 0}^{n} A (k) B (n - k)) (j) z^{j})$
118	5 11 27 102 117	coeeq	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to coeff (F \times_{f} G) = (n \in ℕ_{0} ⟼ \sum_{k = 0}^{n} A (k) B (n - k))$
119		ffvelcdm	$⊢ ((n \in ℕ_{0} ⟼ \sum_{k = 0}^{n} A (k) B (n - k)) : ℕ_{0} ⟶ ℂ \land j \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ \sum_{k = 0}^{n} A (k) B (n - k)) (j) \in ℂ$
120	27 112 119	syl2an	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land j \in (0 \dots M + N)) \to (n \in ℕ_{0} ⟼ \sum_{k = 0}^{n} A (k) B (n - k)) (j) \in ℂ$
121	5 11 120 117	dgrle	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to \deg (F \times_{f} G) \leq M + N$
122	118 121	jca	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to (coeff (F \times_{f} G) = (n \in ℕ_{0} ⟼ \sum_{k = 0}^{n} A (k) B (n - k)) \land \deg (F \times_{f} G) \leq M + N)$

Metamath Proof Explorer

Theorem coemullem

Proof