Metamath Proof Explorer


Theorem coemulhi

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

Ref Expression
Hypotheses coefv0.1 𝐴 = ( coeff ‘ 𝐹 )
coeadd.2 𝐵 = ( coeff ‘ 𝐺 )
coemulhi.3 𝑀 = ( deg ‘ 𝐹 )
coemulhi.4 𝑁 = ( deg ‘ 𝐺 )
Assertion coemulhi ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( coeff ‘ ( 𝐹f · 𝐺 ) ) ‘ ( 𝑀 + 𝑁 ) ) = ( ( 𝐴𝑀 ) · ( 𝐵𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 coefv0.1 𝐴 = ( coeff ‘ 𝐹 )
2 coeadd.2 𝐵 = ( coeff ‘ 𝐺 )
3 coemulhi.3 𝑀 = ( deg ‘ 𝐹 )
4 coemulhi.4 𝑁 = ( deg ‘ 𝐺 )
5 dgrcl ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
6 3 5 eqeltrid ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝑀 ∈ ℕ0 )
7 dgrcl ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐺 ) ∈ ℕ0 )
8 4 7 eqeltrid ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → 𝑁 ∈ ℕ0 )
9 nn0addcl ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( 𝑀 + 𝑁 ) ∈ ℕ0 )
10 6 8 9 syl2an ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝑀 + 𝑁 ) ∈ ℕ0 )
11 1 2 coemul ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( ( coeff ‘ ( 𝐹f · 𝐺 ) ) ‘ ( 𝑀 + 𝑁 ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( ( 𝐴𝑘 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) )
12 10 11 mpd3an3 ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( coeff ‘ ( 𝐹f · 𝐺 ) ) ‘ ( 𝑀 + 𝑁 ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( ( 𝐴𝑘 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) )
13 8 adantl ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝑁 ∈ ℕ0 )
14 13 nn0ge0d ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 0 ≤ 𝑁 )
15 6 adantr ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝑀 ∈ ℕ0 )
16 15 nn0red ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝑀 ∈ ℝ )
17 13 nn0red ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝑁 ∈ ℝ )
18 16 17 addge01d ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 0 ≤ 𝑁𝑀 ≤ ( 𝑀 + 𝑁 ) ) )
19 14 18 mpbid ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝑀 ≤ ( 𝑀 + 𝑁 ) )
20 nn0uz 0 = ( ℤ ‘ 0 )
21 15 20 eleqtrdi ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝑀 ∈ ( ℤ ‘ 0 ) )
22 10 nn0zd ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
23 elfz5 ( ( 𝑀 ∈ ( ℤ ‘ 0 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ) → ( 𝑀 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ↔ 𝑀 ≤ ( 𝑀 + 𝑁 ) ) )
24 21 22 23 syl2anc ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝑀 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ↔ 𝑀 ≤ ( 𝑀 + 𝑁 ) ) )
25 19 24 mpbird ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝑀 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) )
26 25 snssd ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → { 𝑀 } ⊆ ( 0 ... ( 𝑀 + 𝑁 ) ) )
27 elsni ( 𝑘 ∈ { 𝑀 } → 𝑘 = 𝑀 )
28 27 adantl ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ { 𝑀 } ) → 𝑘 = 𝑀 )
29 fveq2 ( 𝑘 = 𝑀 → ( 𝐴𝑘 ) = ( 𝐴𝑀 ) )
30 oveq2 ( 𝑘 = 𝑀 → ( ( 𝑀 + 𝑁 ) − 𝑘 ) = ( ( 𝑀 + 𝑁 ) − 𝑀 ) )
31 30 fveq2d ( 𝑘 = 𝑀 → ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) = ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑀 ) ) )
32 29 31 oveq12d ( 𝑘 = 𝑀 → ( ( 𝐴𝑘 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) = ( ( 𝐴𝑀 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑀 ) ) ) )
33 28 32 syl ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ { 𝑀 } ) → ( ( 𝐴𝑘 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) = ( ( 𝐴𝑀 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑀 ) ) ) )
34 16 recnd ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝑀 ∈ ℂ )
35 17 recnd ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝑁 ∈ ℂ )
36 34 35 pncan2d ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( 𝑀 + 𝑁 ) − 𝑀 ) = 𝑁 )
37 36 fveq2d ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑀 ) ) = ( 𝐵𝑁 ) )
38 37 oveq2d ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( 𝐴𝑀 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑀 ) ) ) = ( ( 𝐴𝑀 ) · ( 𝐵𝑁 ) ) )
39 1 coef3 ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐴 : ℕ0 ⟶ ℂ )
40 39 adantr ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝐴 : ℕ0 ⟶ ℂ )
41 40 15 ffvelrnd ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐴𝑀 ) ∈ ℂ )
42 2 coef3 ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → 𝐵 : ℕ0 ⟶ ℂ )
43 42 adantl ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝐵 : ℕ0 ⟶ ℂ )
44 43 13 ffvelrnd ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐵𝑁 ) ∈ ℂ )
45 41 44 mulcld ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( 𝐴𝑀 ) · ( 𝐵𝑁 ) ) ∈ ℂ )
46 38 45 eqeltrd ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( 𝐴𝑀 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑀 ) ) ) ∈ ℂ )
47 46 adantr ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ { 𝑀 } ) → ( ( 𝐴𝑀 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑀 ) ) ) ∈ ℂ )
48 33 47 eqeltrd ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ { 𝑀 } ) → ( ( 𝐴𝑘 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) ∈ ℂ )
49 simpl ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
50 eldifi ( 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) → 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) )
51 elfznn0 ( 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) → 𝑘 ∈ ℕ0 )
52 50 51 syl ( 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) → 𝑘 ∈ ℕ0 )
53 1 3 dgrub ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ℕ0 ∧ ( 𝐴𝑘 ) ≠ 0 ) → 𝑘𝑀 )
54 53 3expia ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴𝑘 ) ≠ 0 → 𝑘𝑀 ) )
55 49 52 54 syl2an ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → ( ( 𝐴𝑘 ) ≠ 0 → 𝑘𝑀 ) )
56 55 necon1bd ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → ( ¬ 𝑘𝑀 → ( 𝐴𝑘 ) = 0 ) )
57 56 imp ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) ∧ ¬ 𝑘𝑀 ) → ( 𝐴𝑘 ) = 0 )
58 57 oveq1d ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) ∧ ¬ 𝑘𝑀 ) → ( ( 𝐴𝑘 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) = ( 0 · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) )
59 43 ad2antrr ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) ∧ ¬ 𝑘𝑀 ) → 𝐵 : ℕ0 ⟶ ℂ )
60 50 ad2antlr ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) ∧ ¬ 𝑘𝑀 ) → 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) )
61 fznn0sub ( 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) → ( ( 𝑀 + 𝑁 ) − 𝑘 ) ∈ ℕ0 )
62 60 61 syl ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) ∧ ¬ 𝑘𝑀 ) → ( ( 𝑀 + 𝑁 ) − 𝑘 ) ∈ ℕ0 )
63 59 62 ffvelrnd ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) ∧ ¬ 𝑘𝑀 ) → ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ∈ ℂ )
64 63 mul02d ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) ∧ ¬ 𝑘𝑀 ) → ( 0 · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) = 0 )
65 58 64 eqtrd ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) ∧ ¬ 𝑘𝑀 ) → ( ( 𝐴𝑘 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) = 0 )
66 16 adantr ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → 𝑀 ∈ ℝ )
67 50 adantl ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) )
68 67 51 syl ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → 𝑘 ∈ ℕ0 )
69 68 nn0red ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → 𝑘 ∈ ℝ )
70 17 adantr ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → 𝑁 ∈ ℝ )
71 66 69 70 leadd1d ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → ( 𝑀𝑘 ↔ ( 𝑀 + 𝑁 ) ≤ ( 𝑘 + 𝑁 ) ) )
72 10 adantr ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → ( 𝑀 + 𝑁 ) ∈ ℕ0 )
73 72 nn0red ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → ( 𝑀 + 𝑁 ) ∈ ℝ )
74 73 69 70 lesubadd2d ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → ( ( ( 𝑀 + 𝑁 ) − 𝑘 ) ≤ 𝑁 ↔ ( 𝑀 + 𝑁 ) ≤ ( 𝑘 + 𝑁 ) ) )
75 71 74 bitr4d ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → ( 𝑀𝑘 ↔ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ≤ 𝑁 ) )
76 75 notbid ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → ( ¬ 𝑀𝑘 ↔ ¬ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ≤ 𝑁 ) )
77 76 biimpa ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) ∧ ¬ 𝑀𝑘 ) → ¬ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ≤ 𝑁 )
78 simpr ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
79 50 61 syl ( 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) → ( ( 𝑀 + 𝑁 ) − 𝑘 ) ∈ ℕ0 )
80 2 4 dgrub ( ( 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ∈ ℕ0 ∧ ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ≠ 0 ) → ( ( 𝑀 + 𝑁 ) − 𝑘 ) ≤ 𝑁 )
81 80 3expia ( ( 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ∈ ℕ0 ) → ( ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ≠ 0 → ( ( 𝑀 + 𝑁 ) − 𝑘 ) ≤ 𝑁 ) )
82 78 79 81 syl2an ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → ( ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ≠ 0 → ( ( 𝑀 + 𝑁 ) − 𝑘 ) ≤ 𝑁 ) )
83 82 necon1bd ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → ( ¬ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ≤ 𝑁 → ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) = 0 ) )
84 83 imp ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) ∧ ¬ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ≤ 𝑁 ) → ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) = 0 )
85 77 84 syldan ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) ∧ ¬ 𝑀𝑘 ) → ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) = 0 )
86 85 oveq2d ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) ∧ ¬ 𝑀𝑘 ) → ( ( 𝐴𝑘 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) = ( ( 𝐴𝑘 ) · 0 ) )
87 40 ad2antrr ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) ∧ ¬ 𝑀𝑘 ) → 𝐴 : ℕ0 ⟶ ℂ )
88 52 ad2antlr ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) ∧ ¬ 𝑀𝑘 ) → 𝑘 ∈ ℕ0 )
89 87 88 ffvelrnd ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) ∧ ¬ 𝑀𝑘 ) → ( 𝐴𝑘 ) ∈ ℂ )
90 89 mul01d ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) ∧ ¬ 𝑀𝑘 ) → ( ( 𝐴𝑘 ) · 0 ) = 0 )
91 86 90 eqtrd ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) ∧ ¬ 𝑀𝑘 ) → ( ( 𝐴𝑘 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) = 0 )
92 eldifsni ( 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) → 𝑘𝑀 )
93 92 adantl ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → 𝑘𝑀 )
94 69 66 letri3d ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → ( 𝑘 = 𝑀 ↔ ( 𝑘𝑀𝑀𝑘 ) ) )
95 94 necon3abid ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → ( 𝑘𝑀 ↔ ¬ ( 𝑘𝑀𝑀𝑘 ) ) )
96 93 95 mpbid ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → ¬ ( 𝑘𝑀𝑀𝑘 ) )
97 ianor ( ¬ ( 𝑘𝑀𝑀𝑘 ) ↔ ( ¬ 𝑘𝑀 ∨ ¬ 𝑀𝑘 ) )
98 96 97 sylib ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → ( ¬ 𝑘𝑀 ∨ ¬ 𝑀𝑘 ) )
99 65 91 98 mpjaodan ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → ( ( 𝐴𝑘 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) = 0 )
100 fzfid ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 0 ... ( 𝑀 + 𝑁 ) ) ∈ Fin )
101 26 48 99 100 fsumss ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → Σ 𝑘 ∈ { 𝑀 } ( ( 𝐴𝑘 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( ( 𝐴𝑘 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) )
102 32 sumsn ( ( 𝑀 ∈ ℕ0 ∧ ( ( 𝐴𝑀 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑀 ) ) ) ∈ ℂ ) → Σ 𝑘 ∈ { 𝑀 } ( ( 𝐴𝑘 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) = ( ( 𝐴𝑀 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑀 ) ) ) )
103 15 46 102 syl2anc ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → Σ 𝑘 ∈ { 𝑀 } ( ( 𝐴𝑘 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) = ( ( 𝐴𝑀 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑀 ) ) ) )
104 103 38 eqtrd ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → Σ 𝑘 ∈ { 𝑀 } ( ( 𝐴𝑘 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) = ( ( 𝐴𝑀 ) · ( 𝐵𝑁 ) ) )
105 12 101 104 3eqtr2d ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( coeff ‘ ( 𝐹f · 𝐺 ) ) ‘ ( 𝑀 + 𝑁 ) ) = ( ( 𝐴𝑀 ) · ( 𝐵𝑁 ) ) )