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