Metamath Proof Explorer


Theorem signsplypnf

Description: The quotient of a polynomial F by a monic monomial of same degree G converges to the highest coefficient of F . (Contributed by Thierry Arnoux, 18-Sep-2018)

Ref Expression
Hypotheses signsply0.d D=degF
signsply0.c C=coeffF
signsply0.b B=CD
signsplypnf.g G=x+xD
Assertion signsplypnf FPolyF÷fGB

Proof

Step Hyp Ref Expression
1 signsply0.d D=degF
2 signsply0.c C=coeffF
3 signsply0.b B=CD
4 signsplypnf.g G=x+xD
5 plyf FPolyF:
6 5 ffnd FPolyFFn
7 ovex xDV
8 7 rgenw x+xDV
9 4 fnmpt x+xDVGFn+
10 8 9 mp1i FPolyGFn+
11 cnex V
12 11 a1i FPolyV
13 reex V
14 rpssre +
15 13 14 ssexi +V
16 15 a1i FPoly+V
17 ax-resscn
18 14 17 sstri +
19 sseqin2 ++=+
20 18 19 mpbi +=+
21 2 1 coeid2 FPolyxFx=k=0DCkxk
22 4 fvmpt2 x+xDVGx=xD
23 7 22 mpan2 x+Gx=xD
24 23 adantl FPolyx+Gx=xD
25 6 10 12 16 20 21 24 offval FPolyF÷fG=x+k=0DCkxkxD
26 fzfid FPolyx+0DFin
27 18 a1i FPoly+
28 27 sselda FPolyx+x
29 dgrcl FPolydegF0
30 1 29 eqeltrid FPolyD0
31 30 adantr FPolyx+D0
32 28 31 expcld FPolyx+xD
33 2 coef3 FPolyC:0
34 33 ad2antrr FPolyx+k0DC:0
35 elfznn0 k0Dk0
36 35 adantl FPolyx+k0Dk0
37 34 36 ffvelrnd FPolyx+k0DCk
38 28 adantr FPolyx+k0Dx
39 38 36 expcld FPolyx+k0Dxk
40 37 39 mulcld FPolyx+k0DCkxk
41 rpne0 x+x0
42 41 adantl FPolyx+x0
43 30 nn0zd FPolyD
44 43 adantr FPolyx+D
45 28 42 44 expne0d FPolyx+xD0
46 26 32 40 45 fsumdivc FPolyx+k=0DCkxkxD=k=0DCkxkxD
47 fzosn DD..^D+1=D
48 47 ineq2d D0..^DD..^D+1=0..^DD
49 fzodisj 0..^DD..^D+1=
50 48 49 eqtr3di D0..^DD=
51 44 50 syl FPolyx+0..^DD=
52 fzval3 D0D=0..^D+1
53 43 52 syl FPoly0D=0..^D+1
54 nn0uz 0=0
55 30 54 eleqtrdi FPolyD0
56 fzosplitsn D00..^D+1=0..^DD
57 55 56 syl FPoly0..^D+1=0..^DD
58 53 57 eqtrd FPoly0D=0..^DD
59 58 adantr FPolyx+0D=0..^DD
60 32 adantr FPolyx+k0DxD
61 42 adantr FPolyx+k0Dx0
62 44 adantr FPolyx+k0DD
63 38 61 62 expne0d FPolyx+k0DxD0
64 40 60 63 divcld FPolyx+k0DCkxkxD
65 51 59 26 64 fsumsplit FPolyx+k=0DCkxkxD=k0..^DCkxkxD+kDCkxkxD
66 46 65 eqtrd FPolyx+k=0DCkxkxD=k0..^DCkxkxD+kDCkxkxD
67 66 mpteq2dva FPolyx+k=0DCkxkxD=x+k0..^DCkxkxD+kDCkxkxD
68 25 67 eqtrd FPolyF÷fG=x+k0..^DCkxkxD+kDCkxkxD
69 sumex k0..^DCkxkxDV
70 69 a1i FPolyx+k0..^DCkxkxDV
71 sumex kDCkxkxDV
72 71 a1i FPolyx+kDCkxkxDV
73 14 a1i FPoly+
74 fzofi 0..^DFin
75 74 a1i FPoly0..^DFin
76 ovexd FPolyx+k0..^DCkxkxDV
77 33 ad2antrr FPolyk0..^Dx+C:0
78 elfzonn0 k0..^Dk0
79 78 ad2antlr FPolyk0..^Dx+k0
80 77 79 ffvelrnd FPolyk0..^Dx+Ck
81 28 adantlr FPolyk0..^Dx+x
82 81 79 expcld FPolyk0..^Dx+xk
83 32 adantlr FPolyk0..^Dx+xD
84 41 adantl FPolyk0..^Dx+x0
85 44 adantlr FPolyk0..^Dx+D
86 81 84 85 expne0d FPolyk0..^Dx+xD0
87 80 82 83 86 divassd FPolyk0..^Dx+CkxkxD=CkxkxD
88 87 mpteq2dva FPolyk0..^Dx+CkxkxD=x+CkxkxD
89 fvexd FPolyk0..^Dx+CkV
90 ovexd FPolyk0..^Dx+xkxDV
91 33 adantr FPolyk0..^DC:0
92 78 adantl FPolyk0..^Dk0
93 91 92 ffvelrnd FPolyk0..^DCk
94 rlimconst +Ckx+CkCk
95 14 93 94 sylancr FPolyk0..^Dx+CkCk
96 79 nn0zd FPolyk0..^Dx+k
97 85 96 zsubcld FPolyk0..^Dx+Dk
98 81 84 97 cxpexpzd FPolyk0..^Dx+xDk=xDk
99 98 oveq2d FPolyk0..^Dx+1xDk=1xDk
100 81 84 97 expnegd FPolyk0..^Dx+xDk=1xDk
101 85 zcnd FPolyk0..^Dx+D
102 79 nn0cnd FPolyk0..^Dx+k
103 101 102 negsubdi2d FPolyk0..^Dx+Dk=kD
104 103 oveq2d FPolyk0..^Dx+xDk=xkD
105 99 100 104 3eqtr2d FPolyk0..^Dx+1xDk=xkD
106 81 84 85 96 expsubd FPolyk0..^Dx+xkD=xkxD
107 105 106 eqtrd FPolyk0..^Dx+1xDk=xkxD
108 107 mpteq2dva FPolyk0..^Dx+1xDk=x+xkxD
109 92 nn0red FPolyk0..^Dk
110 30 adantr FPolyk0..^DD0
111 110 nn0red FPolyk0..^DD
112 elfzolt2 k0..^Dk<D
113 112 adantl FPolyk0..^Dk<D
114 difrp kDk<DDk+
115 114 biimpa kDk<DDk+
116 109 111 113 115 syl21anc FPolyk0..^DDk+
117 cxplim Dk+x+1xDk0
118 116 117 syl FPolyk0..^Dx+1xDk0
119 108 118 eqbrtrrd FPolyk0..^Dx+xkxD0
120 89 90 95 119 rlimmul FPolyk0..^Dx+CkxkxDCk0
121 93 mul01d FPolyk0..^DCk0=0
122 120 121 breqtrd FPolyk0..^Dx+CkxkxD0
123 88 122 eqbrtrd FPolyk0..^Dx+CkxkxD0
124 73 75 76 123 fsumrlim FPolyx+k0..^DCkxkxDk0..^D0
125 75 olcd FPoly0..^D00..^DFin
126 sumz 0..^D00..^DFink0..^D0=0
127 125 126 syl FPolyk0..^D0=0
128 124 127 breqtrd FPolyx+k0..^DCkxkxD0
129 33 30 ffvelrnd FPolyCD
130 129 adantr FPolyx+CD
131 130 32 mulcld FPolyx+CDxD
132 131 32 45 divcld FPolyx+CDxDxD
133 fveq2 k=DCk=CD
134 oveq2 k=Dxk=xD
135 133 134 oveq12d k=DCkxk=CDxD
136 135 oveq1d k=DCkxkxD=CDxDxD
137 136 sumsn D0CDxDxDkDCkxkxD=CDxDxD
138 31 132 137 syl2anc FPolyx+kDCkxkxD=CDxDxD
139 130 32 45 divcan4d FPolyx+CDxDxD=CD
140 138 139 eqtrd FPolyx+kDCkxkxD=CD
141 140 mpteq2dva FPolyx+kDCkxkxD=x+CD
142 rlimconst +CDx+CDCD
143 14 129 142 sylancr FPolyx+CDCD
144 141 143 eqbrtrd FPolyx+kDCkxkxDCD
145 70 72 128 144 rlimadd FPolyx+k0..^DCkxkxD+kDCkxkxD0+CD
146 129 addid2d FPoly0+CD=CD
147 146 3 eqtr4di FPoly0+CD=B
148 145 147 breqtrd FPolyx+k0..^DCkxkxD+kDCkxkxDB
149 68 148 eqbrtrd FPolyF÷fGB