coemulhi

Description: The leading coefficient of a product of polynomials. (Contributed by Mario Carneiro, 24-Jul-2014)

	Ref	Expression
Hypotheses	coefv0.1	$⊢ A = coeff (F)$
	coeadd.2	$⊢ B = coeff (G)$
	coemulhi.3	$⊢ M = \deg (F)$
	coemulhi.4	$⊢ N = \deg (G)$
Assertion	coemulhi	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to coeff (F \times_{f} G) (M + N) = A (M) B (N)$

Proof

Step	Hyp	Ref	Expression
1		coefv0.1	$⊢ A = coeff (F)$
2		coeadd.2	$⊢ B = coeff (G)$
3		coemulhi.3	$⊢ M = \deg (F)$
4		coemulhi.4	$⊢ N = \deg (G)$
5		dgrcl	$⊢ F \in Poly (S) \to \deg (F) \in ℕ_{0}$
6	3 5	eqeltrid	$⊢ F \in Poly (S) \to M \in ℕ_{0}$
7		dgrcl	$⊢ G \in Poly (S) \to \deg (G) \in ℕ_{0}$
8	4 7	eqeltrid	$⊢ G \in Poly (S) \to N \in ℕ_{0}$
9		nn0addcl	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to M + N \in ℕ_{0}$
10	6 8 9	syl2an	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to M + N \in ℕ_{0}$
11	1 2	coemul	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M + N \in ℕ_{0}) \to coeff (F \times_{f} G) (M + N) = \sum_{k = 0}^{M + N} A (k) B (M + N - k)$
12	10 11	mpd3an3	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to coeff (F \times_{f} G) (M + N) = \sum_{k = 0}^{M + N} A (k) B (M + N - k)$
13	8	adantl	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to N \in ℕ_{0}$
14	13	nn0ge0d	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to 0 \leq N$
15	6	adantr	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to M \in ℕ_{0}$
16	15	nn0red	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to M \in ℝ$
17	13	nn0red	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to N \in ℝ$
18	16 17	addge01d	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to (0 \leq N \leftrightarrow M \leq M + N)$
19	14 18	mpbid	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to M \leq M + N$
20		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
21	15 20	eleqtrdi	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to M \in ℤ_{\geq 0}$
22	10	nn0zd	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to M + N \in ℤ$
23		elfz5	$⊢ (M \in ℤ_{\geq 0} \land M + N \in ℤ) \to (M \in (0 \dots M + N) \leftrightarrow M \leq M + N)$
24	21 22 23	syl2anc	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to (M \in (0 \dots M + N) \leftrightarrow M \leq M + N)$
25	19 24	mpbird	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to M \in (0 \dots M + N)$
26	25	snssd	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to \{M\} \subseteq (0 \dots M + N)$
27		elsni	$⊢ k \in \{M\} \to k = M$
28	27	adantl	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in \{M\}) \to k = M$
29		fveq2	$⊢ k = M \to A (k) = A (M)$
30		oveq2	$⊢ k = M \to M + N - k = M + N - M$
31	30	fveq2d	$⊢ k = M \to B (M + N - k) = B (M + N - M)$
32	29 31	oveq12d	$⊢ k = M \to A (k) B (M + N - k) = A (M) B (M + N - M)$
33	28 32	syl	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in \{M\}) \to A (k) B (M + N - k) = A (M) B (M + N - M)$
34	16	recnd	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to M \in ℂ$
35	17	recnd	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to N \in ℂ$
36	34 35	pncan2d	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to M + N - M = N$
37	36	fveq2d	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to B (M + N - M) = B (N)$
38	37	oveq2d	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to A (M) B (M + N - M) = A (M) B (N)$
39	1	coef3	$⊢ F \in Poly (S) \to A : ℕ_{0} ⟶ ℂ$
40	39	adantr	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to A : ℕ_{0} ⟶ ℂ$
41	40 15	ffvelcdmd	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to A (M) \in ℂ$
42	2	coef3	$⊢ G \in Poly (S) \to B : ℕ_{0} ⟶ ℂ$
43	42	adantl	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to B : ℕ_{0} ⟶ ℂ$
44	43 13	ffvelcdmd	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to B (N) \in ℂ$
45	41 44	mulcld	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to A (M) B (N) \in ℂ$
46	38 45	eqeltrd	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to A (M) B (M + N - M) \in ℂ$
47	46	adantr	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in \{M\}) \to A (M) B (M + N - M) \in ℂ$
48	33 47	eqeltrd	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in \{M\}) \to A (k) B (M + N - k) \in ℂ$
49		simpl	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to F \in Poly (S)$
50		eldifi	$⊢ k \in ((0 \dots M + N) ∖ \{M\}) \to k \in (0 \dots M + N)$
51		elfznn0	$⊢ k \in (0 \dots M + N) \to k \in ℕ_{0}$
52	50 51	syl	$⊢ k \in ((0 \dots M + N) ∖ \{M\}) \to k \in ℕ_{0}$
53	1 3	dgrub	$⊢ (F \in Poly (S) \land k \in ℕ_{0} \land A (k) \neq 0) \to k \leq M$
54	53	3expia	$⊢ (F \in Poly (S) \land k \in ℕ_{0}) \to (A (k) \neq 0 \to k \leq M)$
55	49 52 54	syl2an	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \to (A (k) \neq 0 \to k \leq M)$
56	55	necon1bd	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \to (\neg k \leq M \to A (k) = 0)$
57	56	imp	$⊢ (((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \land \neg k \leq M) \to A (k) = 0$
58	57	oveq1d	$⊢ (((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \land \neg k \leq M) \to A (k) B (M + N - k) = 0 \cdot B (M + N - k)$
59	43	ad2antrr	$⊢ (((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \land \neg k \leq M) \to B : ℕ_{0} ⟶ ℂ$
60	50	ad2antlr	$⊢ (((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \land \neg k \leq M) \to k \in (0 \dots M + N)$
61		fznn0sub	$⊢ k \in (0 \dots M + N) \to M + N - k \in ℕ_{0}$
62	60 61	syl	$⊢ (((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \land \neg k \leq M) \to M + N - k \in ℕ_{0}$
63	59 62	ffvelcdmd	$⊢ (((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \land \neg k \leq M) \to B (M + N - k) \in ℂ$
64	63	mul02d	$⊢ (((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \land \neg k \leq M) \to 0 \cdot B (M + N - k) = 0$
65	58 64	eqtrd	$⊢ (((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \land \neg k \leq M) \to A (k) B (M + N - k) = 0$
66	16	adantr	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \to M \in ℝ$
67	50	adantl	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \to k \in (0 \dots M + N)$
68	67 51	syl	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \to k \in ℕ_{0}$
69	68	nn0red	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \to k \in ℝ$
70	17	adantr	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \to N \in ℝ$
71	66 69 70	leadd1d	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \to (M \leq k \leftrightarrow M + N \leq k + N)$
72	10	adantr	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \to M + N \in ℕ_{0}$
73	72	nn0red	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \to M + N \in ℝ$
74	73 69 70	lesubadd2d	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \to (M + N - k \leq N \leftrightarrow M + N \leq k + N)$
75	71 74	bitr4d	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \to (M \leq k \leftrightarrow M + N - k \leq N)$
76	75	notbid	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \to (\neg M \leq k \leftrightarrow \neg M + N - k \leq N)$
77	76	biimpa	$⊢ (((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \land \neg M \leq k) \to \neg M + N - k \leq N$
78		simpr	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to G \in Poly (S)$
79	50 61	syl	$⊢ k \in ((0 \dots M + N) ∖ \{M\}) \to M + N - k \in ℕ_{0}$
80	2 4	dgrub	$⊢ (G \in Poly (S) \land M + N - k \in ℕ_{0} \land B (M + N - k) \neq 0) \to M + N - k \leq N$
81	80	3expia	$⊢ (G \in Poly (S) \land M + N - k \in ℕ_{0}) \to (B (M + N - k) \neq 0 \to M + N - k \leq N)$
82	78 79 81	syl2an	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \to (B (M + N - k) \neq 0 \to M + N - k \leq N)$
83	82	necon1bd	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \to (\neg M + N - k \leq N \to B (M + N - k) = 0)$
84	83	imp	$⊢ (((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \land \neg M + N - k \leq N) \to B (M + N - k) = 0$
85	77 84	syldan	$⊢ (((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \land \neg M \leq k) \to B (M + N - k) = 0$
86	85	oveq2d	$⊢ (((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \land \neg M \leq k) \to A (k) B (M + N - k) = A (k) \cdot 0$
87	40	ad2antrr	$⊢ (((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \land \neg M \leq k) \to A : ℕ_{0} ⟶ ℂ$
88	52	ad2antlr	$⊢ (((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \land \neg M \leq k) \to k \in ℕ_{0}$
89	87 88	ffvelcdmd	$⊢ (((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \land \neg M \leq k) \to A (k) \in ℂ$
90	89	mul01d	$⊢ (((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \land \neg M \leq k) \to A (k) \cdot 0 = 0$
91	86 90	eqtrd	$⊢ (((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \land \neg M \leq k) \to A (k) B (M + N - k) = 0$
92		eldifsni	$⊢ k \in ((0 \dots M + N) ∖ \{M\}) \to k \neq M$
93	92	adantl	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \to k \neq M$
94	69 66	letri3d	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \to (k = M \leftrightarrow (k \leq M \land M \leq k))$
95	94	necon3abid	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \to (k \neq M \leftrightarrow \neg (k \leq M \land M \leq k))$
96	93 95	mpbid	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \to \neg (k \leq M \land M \leq k)$
97		ianor	$⊢ \neg (k \leq M \land M \leq k) \leftrightarrow (\neg k \leq M \lor \neg M \leq k)$
98	96 97	sylib	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \to (\neg k \leq M \lor \neg M \leq k)$
99	65 91 98	mpjaodan	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ((0 \dots M + N) ∖ \{M\})) \to A (k) B (M + N - k) = 0$
100		fzfid	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to (0 \dots M + N) \in Fin$
101	26 48 99 100	fsumss	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to \sum_{k \in \{M\}} A (k) B (M + N - k) = \sum_{k = 0}^{M + N} A (k) B (M + N - k)$
102	32	sumsn	$⊢ (M \in ℕ_{0} \land A (M) B (M + N - M) \in ℂ) \to \sum_{k \in \{M\}} A (k) B (M + N - k) = A (M) B (M + N - M)$
103	15 46 102	syl2anc	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to \sum_{k \in \{M\}} A (k) B (M + N - k) = A (M) B (M + N - M)$
104	103 38	eqtrd	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to \sum_{k \in \{M\}} A (k) B (M + N - k) = A (M) B (N)$
105	12 101 104	3eqtr2d	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to coeff (F \times_{f} G) (M + N) = A (M) B (N)$

Metamath Proof Explorer

Theorem coemulhi

Proof