Proof of Theorem plydivlem4
Step | Hyp | Ref
| Expression |
1 | | plydiv.f |
. . . . . . . 8
Poly |
2 | | plybss 23950 |
. . . . . . . 8
Poly
|
3 | 1, 2 | syl 17 |
. . . . . . 7
|
4 | | plydiv.pl |
. . . . . . . . . . . . 13
|
5 | | plydiv.tm |
. . . . . . . . . . . . 13
|
6 | | plydiv.rc |
. . . . . . . . . . . . 13
|
7 | | plydiv.m1 |
. . . . . . . . . . . . 13
|
8 | 4, 5, 6, 7 | plydivlem1 24048 |
. . . . . . . . . . . 12
|
9 | | plydiv.a |
. . . . . . . . . . . . 13
coeff |
10 | 9 | coef2 23987 |
. . . . . . . . . . . 12
Poly |
11 | 1, 8, 10 | syl2anc 693 |
. . . . . . . . . . 11
|
12 | | plydiv.m |
. . . . . . . . . . . 12
deg |
13 | | dgrcl 23989 |
. . . . . . . . . . . . 13
Poly
deg |
14 | 1, 13 | syl 17 |
. . . . . . . . . . . 12
deg |
15 | 12, 14 | syl5eqel 2705 |
. . . . . . . . . . 11
|
16 | 11, 15 | ffvelrnd 6360 |
. . . . . . . . . 10
|
17 | 3, 16 | sseldd 3604 |
. . . . . . . . 9
|
18 | | plydiv.g |
. . . . . . . . . . . 12
Poly |
19 | | plydiv.b |
. . . . . . . . . . . . 13
coeff |
20 | 19 | coef2 23987 |
. . . . . . . . . . . 12
Poly |
21 | 18, 8, 20 | syl2anc 693 |
. . . . . . . . . . 11
|
22 | | plydiv.n |
. . . . . . . . . . . 12
deg |
23 | | dgrcl 23989 |
. . . . . . . . . . . . 13
Poly
deg |
24 | 18, 23 | syl 17 |
. . . . . . . . . . . 12
deg |
25 | 22, 24 | syl5eqel 2705 |
. . . . . . . . . . 11
|
26 | 21, 25 | ffvelrnd 6360 |
. . . . . . . . . 10
|
27 | 3, 26 | sseldd 3604 |
. . . . . . . . 9
|
28 | | plydiv.z |
. . . . . . . . . 10
|
29 | 22, 19 | dgreq0 24021 |
. . . . . . . . . . . 12
Poly
|
30 | 18, 29 | syl 17 |
. . . . . . . . . . 11
|
31 | 30 | necon3bid 2838 |
. . . . . . . . . 10
|
32 | 28, 31 | mpbid 222 |
. . . . . . . . 9
|
33 | 17, 27, 32 | divrecd 10804 |
. . . . . . . 8
|
34 | | fvex 6201 |
. . . . . . . . . . . 12
|
35 | | eleq1 2689 |
. . . . . . . . . . . . . . 15
|
36 | | neeq1 2856 |
. . . . . . . . . . . . . . 15
|
37 | 35, 36 | anbi12d 747 |
. . . . . . . . . . . . . 14
|
38 | 37 | anbi2d 740 |
. . . . . . . . . . . . 13
|
39 | | oveq2 6658 |
. . . . . . . . . . . . . 14
|
40 | 39 | eleq1d 2686 |
. . . . . . . . . . . . 13
|
41 | 38, 40 | imbi12d 334 |
. . . . . . . . . . . 12
|
42 | 34, 41, 6 | vtocl 3259 |
. . . . . . . . . . 11
|
43 | 42 | ex 450 |
. . . . . . . . . 10
|
44 | 26, 32, 43 | mp2and 715 |
. . . . . . . . 9
|
45 | 5, 16, 44 | caovcld 6827 |
. . . . . . . 8
|
46 | 33, 45 | eqeltrd 2701 |
. . . . . . 7
|
47 | | plydiv.d |
. . . . . . 7
|
48 | | plydiv.h |
. . . . . . . 8
|
49 | 48 | ply1term 23960 |
. . . . . . 7
Poly |
50 | 3, 46, 47, 49 | syl3anc 1326 |
. . . . . 6
Poly |
51 | 50 | adantr 481 |
. . . . 5
Poly Poly |
52 | | simpr 477 |
. . . . 5
Poly Poly |
53 | 4 | adantlr 751 |
. . . . 5
Poly
|
54 | 51, 52, 53 | plyadd 23973 |
. . . 4
Poly
Poly |
55 | 54 | adantr 481 |
. . 3
Poly
deg
Poly |
56 | | cnex 10017 |
. . . . . . . . 9
|
57 | 56 | a1i 11 |
. . . . . . . 8
Poly |
58 | 1 | adantr 481 |
. . . . . . . . 9
Poly Poly |
59 | | plyf 23954 |
. . . . . . . . 9
Poly
|
60 | 58, 59 | syl 17 |
. . . . . . . 8
Poly |
61 | | mulcl 10020 |
. . . . . . . . . 10
|
62 | 61 | adantl 482 |
. . . . . . . . 9
Poly
|
63 | | plyf 23954 |
. . . . . . . . . 10
Poly
|
64 | 51, 63 | syl 17 |
. . . . . . . . 9
Poly |
65 | 18 | adantr 481 |
. . . . . . . . . 10
Poly Poly |
66 | | plyf 23954 |
. . . . . . . . . 10
Poly
|
67 | 65, 66 | syl 17 |
. . . . . . . . 9
Poly |
68 | | inidm 3822 |
. . . . . . . . 9
|
69 | 62, 64, 67, 57, 57, 68 | off 6912 |
. . . . . . . 8
Poly
|
70 | | plyf 23954 |
. . . . . . . . . 10
Poly
|
71 | 70 | adantl 482 |
. . . . . . . . 9
Poly |
72 | 62, 67, 71, 57, 57, 68 | off 6912 |
. . . . . . . 8
Poly
|
73 | | subsub4 10314 |
. . . . . . . . 9
|
74 | 73 | adantl 482 |
. . . . . . . 8
Poly
|
75 | 57, 60, 69, 72, 74 | caofass 6931 |
. . . . . . 7
Poly
|
76 | | mulcom 10022 |
. . . . . . . . . . . 12
|
77 | 76 | adantl 482 |
. . . . . . . . . . 11
Poly
|
78 | 57, 64, 67, 77 | caofcom 6929 |
. . . . . . . . . 10
Poly
|
79 | 78 | oveq1d 6665 |
. . . . . . . . 9
Poly
|
80 | | adddi 10025 |
. . . . . . . . . . 11
|
81 | 80 | adantl 482 |
. . . . . . . . . 10
Poly
|
82 | 57, 67, 64, 71, 81 | caofdi 6933 |
. . . . . . . . 9
Poly
|
83 | 79, 82 | eqtr4d 2659 |
. . . . . . . 8
Poly
|
84 | 83 | oveq2d 6666 |
. . . . . . 7
Poly
|
85 | 75, 84 | eqtrd 2656 |
. . . . . 6
Poly
|
86 | 85 | eqeq1d 2624 |
. . . . 5
Poly
|
87 | 85 | fveq2d 6195 |
. . . . . 6
Poly deg
deg |
88 | 87 | breq1d 4663 |
. . . . 5
Poly deg
deg
|
89 | 86, 88 | orbi12d 746 |
. . . 4
Poly
deg
deg
|
90 | 89 | biimpa 501 |
. . 3
Poly
deg
deg
|
91 | | plydiv.r |
. . . . . . 7
|
92 | | oveq2 6658 |
. . . . . . . 8
|
93 | 92 | oveq2d 6666 |
. . . . . . 7
|
94 | 91, 93 | syl5eq 2668 |
. . . . . 6
|
95 | 94 | eqeq1d 2624 |
. . . . 5
|
96 | 94 | fveq2d 6195 |
. . . . . 6
deg deg
|
97 | 96 | breq1d 4663 |
. . . . 5
deg
deg |
98 | 95, 97 | orbi12d 746 |
. . . 4
deg deg
|
99 | 98 | rspcev 3309 |
. . 3
Poly
deg
Poly deg |
100 | 55, 90, 99 | syl2anc 693 |
. 2
Poly
deg
Poly deg |
101 | 50, 18, 4, 5 | plymul 23974 |
. . . 4
Poly |
102 | 1, 101, 4, 5, 7 | plysub 23975 |
. . 3
Poly |
103 | | plydiv.al |
. . 3
Poly deg
Poly deg |
104 | | eqid 2622 |
. . . . . . 7
deg
deg
|
105 | 12, 104 | dgrsub 24028 |
. . . . . 6
Poly Poly deg
deg deg |
106 | 1, 101, 105 | syl2anc 693 |
. . . . 5
deg
deg deg |
107 | | plydiv.fz |
. . . . . . . . . . . . 13
|
108 | 12, 9 | dgreq0 24021 |
. . . . . . . . . . . . . . 15
Poly
|
109 | 1, 108 | syl 17 |
. . . . . . . . . . . . . 14
|
110 | 109 | necon3bid 2838 |
. . . . . . . . . . . . 13
|
111 | 107, 110 | mpbid 222 |
. . . . . . . . . . . 12
|
112 | 17, 27, 111, 32 | divne0d 10817 |
. . . . . . . . . . 11
|
113 | 3, 46 | sseldd 3604 |
. . . . . . . . . . . . 13
|
114 | 48 | coe1term 24015 |
. . . . . . . . . . . . 13
coeff |
115 | 113, 47, 47, 114 | syl3anc 1326 |
. . . . . . . . . . . 12
coeff |
116 | | eqid 2622 |
. . . . . . . . . . . . 13
|
117 | 116 | iftruei 4093 |
. . . . . . . . . . . 12
|
118 | 115, 117 | syl6eq 2672 |
. . . . . . . . . . 11
coeff |
119 | | c0ex 10034 |
. . . . . . . . . . . . 13
|
120 | 119 | fvconst2 6469 |
. . . . . . . . . . . 12
|
121 | 47, 120 | syl 17 |
. . . . . . . . . . 11
|
122 | 112, 118,
121 | 3netr4d 2871 |
. . . . . . . . . 10
coeff |
123 | | fveq2 6191 |
. . . . . . . . . . . . 13
coeff coeff |
124 | | coe0 24012 |
. . . . . . . . . . . . 13
coeff |
125 | 123, 124 | syl6eq 2672 |
. . . . . . . . . . . 12
coeff |
126 | 125 | fveq1d 6193 |
. . . . . . . . . . 11
coeff |
127 | 126 | necon3i 2826 |
. . . . . . . . . 10
coeff
|
128 | 122, 127 | syl 17 |
. . . . . . . . 9
|
129 | | eqid 2622 |
. . . . . . . . . 10
deg deg |
130 | 129, 22 | dgrmul 24026 |
. . . . . . . . 9
Poly
Poly deg deg |
131 | 50, 128, 18, 28, 130 | syl22anc 1327 |
. . . . . . . 8
deg
deg |
132 | 48 | dgr1term 24016 |
. . . . . . . . . . . 12
deg |
133 | 113, 112,
47, 132 | syl3anc 1326 |
. . . . . . . . . . 11
deg |
134 | | plydiv.e |
. . . . . . . . . . 11
|
135 | 133, 134 | eqtr4d 2659 |
. . . . . . . . . 10
deg |
136 | 135 | oveq1d 6665 |
. . . . . . . . 9
deg |
137 | 15 | nn0cnd 11353 |
. . . . . . . . . 10
|
138 | 25 | nn0cnd 11353 |
. . . . . . . . . 10
|
139 | 137, 138 | npcand 10396 |
. . . . . . . . 9
|
140 | 136, 139 | eqtrd 2656 |
. . . . . . . 8
deg |
141 | 131, 140 | eqtrd 2656 |
. . . . . . 7
deg
|
142 | 141 | ifeq1d 4104 |
. . . . . 6
deg
deg
deg |
143 | | ifid 4125 |
. . . . . 6
deg |
144 | 142, 143 | syl6eq 2672 |
. . . . 5
deg
deg
|
145 | 106, 144 | breqtrd 4679 |
. . . 4
deg
|
146 | | eqid 2622 |
. . . . . . . 8
coeff
coeff
|
147 | 9, 146 | coesub 24013 |
. . . . . . 7
Poly Poly coeff
coeff |
148 | 1, 101, 147 | syl2anc 693 |
. . . . . 6
coeff
coeff |
149 | 148 | fveq1d 6193 |
. . . . 5
coeff coeff |
150 | 9 | coef3 23988 |
. . . . . . . 8
Poly
|
151 | | ffn 6045 |
. . . . . . . 8
|
152 | 1, 150, 151 | 3syl 18 |
. . . . . . 7
|
153 | 146 | coef3 23988 |
. . . . . . . 8
Poly coeff |
154 | | ffn 6045 |
. . . . . . . 8
coeff coeff |
155 | 101, 153,
154 | 3syl 18 |
. . . . . . 7
coeff
|
156 | | nn0ex 11298 |
. . . . . . . 8
|
157 | 156 | a1i 11 |
. . . . . . 7
|
158 | | inidm 3822 |
. . . . . . 7
|
159 | | eqidd 2623 |
. . . . . . 7
|
160 | | eqid 2622 |
. . . . . . . . . . 11
coeff coeff |
161 | 160, 19, 129, 22 | coemulhi 24010 |
. . . . . . . . . 10
Poly Poly
coeff deg coeffdeg |
162 | 50, 18, 161 | syl2anc 693 |
. . . . . . . . 9
coeff deg coeffdeg |
163 | 140 | fveq2d 6195 |
. . . . . . . . 9
coeff deg coeff |
164 | 133 | fveq2d 6195 |
. . . . . . . . . . . 12
coeffdeg coeff |
165 | 164, 118 | eqtrd 2656 |
. . . . . . . . . . 11
coeffdeg |
166 | 165 | oveq1d 6665 |
. . . . . . . . . 10
coeffdeg |
167 | 17, 27, 32 | divcan1d 10802 |
. . . . . . . . . 10
|
168 | 166, 167 | eqtrd 2656 |
. . . . . . . . 9
coeffdeg |
169 | 162, 163,
168 | 3eqtr3d 2664 |
. . . . . . . 8
coeff |
170 | 169 | adantr 481 |
. . . . . . 7
coeff |
171 | 152, 155,
157, 157, 158, 159, 170 | ofval 6906 |
. . . . . 6
coeff |
172 | 15, 171 | mpdan 702 |
. . . . 5
coeff |
173 | 17 | subidd 10380 |
. . . . 5
|
174 | 149, 172,
173 | 3eqtrd 2660 |
. . . 4
coeff |
175 | | dgrcl 23989 |
. . . . . . . . . 10
Poly deg
|
176 | 102, 175 | syl 17 |
. . . . . . . . 9
deg
|
177 | 176 | nn0red 11352 |
. . . . . . . 8
deg
|
178 | 15 | nn0red 11352 |
. . . . . . . 8
|
179 | 25 | nn0red 11352 |
. . . . . . . 8
|
180 | 177, 178,
179 | ltsub1d 10636 |
. . . . . . 7
deg deg
|
181 | 134 | breq2d 4665 |
. . . . . . 7
deg
deg
|
182 | 180, 181 | bitrd 268 |
. . . . . 6
deg deg
|
183 | 182 | orbi2d 738 |
. . . . 5
deg
deg
|
184 | | eqid 2622 |
. . . . . . 7
deg
deg
|
185 | | eqid 2622 |
. . . . . . 7
coeff
coeff
|
186 | 184, 185 | dgrlt 24022 |
. . . . . 6
Poly
deg
deg
coeff |
187 | 102, 15, 186 | syl2anc 693 |
. . . . 5
deg
deg
coeff |
188 | 183, 187 | bitr3d 270 |
. . . 4
deg
deg
coeff |
189 | 145, 174,
188 | mpbir2and 957 |
. . 3
deg
|
190 | | eqeq1 2626 |
. . . . . 6
|
191 | | fveq2 6191 |
. . . . . . . 8
deg deg
|
192 | 191 | oveq1d 6665 |
. . . . . . 7
deg deg
|
193 | 192 | breq1d 4663 |
. . . . . 6
deg
deg
|
194 | 190, 193 | orbi12d 746 |
. . . . 5
deg deg
|
195 | | plydiv.u |
. . . . . . . . 9
|
196 | | oveq1 6657 |
. . . . . . . . 9
|
197 | 195, 196 | syl5eq 2668 |
. . . . . . . 8
|
198 | 197 | eqeq1d 2624 |
. . . . . . 7
|
199 | 197 | fveq2d 6195 |
. . . . . . . 8
deg deg
|
200 | 199 | breq1d 4663 |
. . . . . . 7
deg deg
|
201 | 198, 200 | orbi12d 746 |
. . . . . 6
deg
deg
|
202 | 201 | rexbidv 3052 |
. . . . 5
Poly deg
Poly
deg
|
203 | 194, 202 | imbi12d 334 |
. . . 4
deg
Poly deg
deg
Poly
deg
|
204 | 203 | rspcv 3305 |
. . 3
Poly Poly deg
Poly deg
deg
Poly
deg
|
205 | 102, 103,
189, 204 | syl3c 66 |
. 2
Poly
deg
|
206 | 100, 205 | r19.29a 3078 |
1
Poly deg |