Step | Hyp | Ref
| Expression |
1 | | plydiv.f |
. . . . . 6
Poly |
2 | | dgrcl 23989 |
. . . . . 6
Poly
deg |
3 | 1, 2 | syl 17 |
. . . . 5
deg |
4 | 3 | nn0red 11352 |
. . . 4
deg |
5 | | plydiv.g |
. . . . . 6
Poly |
6 | | dgrcl 23989 |
. . . . . 6
Poly
deg |
7 | 5, 6 | syl 17 |
. . . . 5
deg |
8 | 7 | nn0red 11352 |
. . . 4
deg |
9 | 4, 8 | resubcld 10458 |
. . 3
deg deg |
10 | | arch 11289 |
. . 3
deg deg deg deg
|
11 | 9, 10 | syl 17 |
. 2
deg deg
|
12 | | olc 399 |
. . . 4
deg deg
deg deg |
13 | 1 | adantr 481 |
. . . . 5
Poly |
14 | | nnnn0 11299 |
. . . . . . 7
|
15 | | breq2 4657 |
. . . . . . . . . . . 12
deg deg deg deg |
16 | 15 | orbi2d 738 |
. . . . . . . . . . 11
deg deg
deg deg |
17 | 16 | imbi1d 331 |
. . . . . . . . . 10
deg deg
Poly
deg
deg deg deg
Poly
deg
deg |
18 | 17 | ralbidv 2986 |
. . . . . . . . 9
Poly deg deg Poly deg
deg
Poly deg deg Poly deg
deg |
19 | 18 | imbi2d 330 |
. . . . . . . 8
Poly deg deg
Poly
deg
deg Poly deg deg Poly deg
deg |
20 | | breq2 4657 |
. . . . . . . . . . . 12
deg deg deg deg |
21 | 20 | orbi2d 738 |
. . . . . . . . . . 11
deg deg
deg deg |
22 | 21 | imbi1d 331 |
. . . . . . . . . 10
deg deg
Poly
deg
deg deg deg
Poly
deg
deg |
23 | 22 | ralbidv 2986 |
. . . . . . . . 9
Poly deg deg Poly deg
deg
Poly deg deg Poly deg
deg |
24 | 23 | imbi2d 330 |
. . . . . . . 8
Poly deg deg
Poly
deg
deg Poly deg deg Poly deg
deg |
25 | | breq2 4657 |
. . . . . . . . . . . 12
deg deg deg deg |
26 | 25 | orbi2d 738 |
. . . . . . . . . . 11
deg deg
deg deg |
27 | 26 | imbi1d 331 |
. . . . . . . . . 10
deg deg
Poly
deg
deg deg deg
Poly
deg
deg |
28 | 27 | ralbidv 2986 |
. . . . . . . . 9
Poly deg deg Poly deg
deg
Poly deg deg Poly deg
deg |
29 | 28 | imbi2d 330 |
. . . . . . . 8
Poly deg deg
Poly
deg
deg Poly deg deg Poly deg
deg |
30 | | plydiv.pl |
. . . . . . . . . . . 12
|
31 | 30 | adantlr 751 |
. . . . . . . . . . 11
Poly deg deg |
32 | | plydiv.tm |
. . . . . . . . . . . 12
|
33 | 32 | adantlr 751 |
. . . . . . . . . . 11
Poly deg deg |
34 | | plydiv.rc |
. . . . . . . . . . . 12
|
35 | 34 | adantlr 751 |
. . . . . . . . . . 11
Poly deg deg |
36 | | plydiv.m1 |
. . . . . . . . . . . 12
|
37 | 36 | adantr 481 |
. . . . . . . . . . 11
Poly deg deg
|
38 | | simprl 794 |
. . . . . . . . . . 11
Poly deg deg
Poly |
39 | 5 | adantr 481 |
. . . . . . . . . . 11
Poly deg deg
Poly |
40 | | plydiv.z |
. . . . . . . . . . . 12
|
41 | 40 | adantr 481 |
. . . . . . . . . . 11
Poly deg deg
|
42 | | eqid 2622 |
. . . . . . . . . . 11
|
43 | | simprr 796 |
. . . . . . . . . . 11
Poly deg deg
deg deg |
44 | 31, 33, 35, 37, 38, 39, 41, 42, 43 | plydivlem3 24050 |
. . . . . . . . . 10
Poly deg deg
Poly deg
deg |
45 | 44 | expr 643 |
. . . . . . . . 9
Poly deg deg Poly deg
deg |
46 | 45 | ralrimiva 2966 |
. . . . . . . 8
Poly deg deg Poly deg
deg |
47 | | eqeq1 2626 |
. . . . . . . . . . . . . . . 16
|
48 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
deg deg |
49 | 48 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
deg deg deg deg |
50 | 49 | breq1d 4663 |
. . . . . . . . . . . . . . . 16
deg deg deg deg |
51 | 47, 50 | orbi12d 746 |
. . . . . . . . . . . . . . 15
deg deg
deg deg |
52 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . 18
|
53 | 52 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . 17
|
54 | 52 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
deg
deg |
55 | 54 | breq1d 4663 |
. . . . . . . . . . . . . . . . 17
deg
deg deg deg |
56 | 53, 55 | orbi12d 746 |
. . . . . . . . . . . . . . . 16
deg
deg
deg
deg |
57 | 56 | rexbidv 3052 |
. . . . . . . . . . . . . . 15
Poly
deg
deg
Poly deg
deg |
58 | 51, 57 | imbi12d 334 |
. . . . . . . . . . . . . 14
deg deg
Poly
deg
deg deg deg
Poly
deg
deg |
59 | 58 | cbvralv 3171 |
. . . . . . . . . . . . 13
Poly deg deg Poly deg
deg
Poly deg deg Poly deg
deg |
60 | | simplll 798 |
. . . . . . . . . . . . . . . . 17
Poly
Poly deg deg Poly deg
deg deg deg |
61 | 60, 30 | sylan 488 |
. . . . . . . . . . . . . . . 16
Poly Poly deg deg Poly deg
deg deg deg
|
62 | 60, 32 | sylan 488 |
. . . . . . . . . . . . . . . 16
Poly Poly deg deg Poly deg
deg deg deg
|
63 | 60, 34 | sylan 488 |
. . . . . . . . . . . . . . . 16
Poly Poly deg deg Poly deg
deg deg deg |
64 | 60, 36 | syl 17 |
. . . . . . . . . . . . . . . 16
Poly
Poly deg deg Poly deg
deg deg deg |
65 | | simplr 792 |
. . . . . . . . . . . . . . . 16
Poly
Poly deg deg Poly deg
deg deg deg Poly |
66 | 60, 5 | syl 17 |
. . . . . . . . . . . . . . . 16
Poly
Poly deg deg Poly deg
deg deg deg Poly |
67 | 60, 40 | syl 17 |
. . . . . . . . . . . . . . . 16
Poly
Poly deg deg Poly deg
deg deg deg |
68 | | simpllr 799 |
. . . . . . . . . . . . . . . 16
Poly
Poly deg deg Poly deg
deg deg deg |
69 | | simprrr 805 |
. . . . . . . . . . . . . . . 16
Poly
Poly deg deg Poly deg
deg deg deg deg deg |
70 | | simprrl 804 |
. . . . . . . . . . . . . . . 16
Poly
Poly deg deg Poly deg
deg deg deg |
71 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
|
72 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . 18
|
73 | 72 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
coeffdeg coeffdeg coeffdeg coeffdeg |
74 | 73 | cbvmptv 4750 |
. . . . . . . . . . . . . . . 16
coeffdeg coeffdeg coeffdeg coeffdeg |
75 | | simprl 794 |
. . . . . . . . . . . . . . . . 17
Poly
Poly deg deg Poly deg
deg deg deg Poly deg deg
Poly
deg
deg |
76 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
77 | 76 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . 22
|
78 | 77 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . 21
|
79 | 77 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . 22
deg
deg |
80 | 79 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . 21
deg
deg deg deg |
81 | 78, 80 | orbi12d 746 |
. . . . . . . . . . . . . . . . . . . 20
deg
deg
deg
deg |
82 | 81 | cbvrexv 3172 |
. . . . . . . . . . . . . . . . . . 19
Poly
deg
deg
Poly deg
deg |
83 | 82 | imbi2i 326 |
. . . . . . . . . . . . . . . . . 18
deg deg
Poly
deg
deg deg deg
Poly
deg
deg |
84 | 83 | ralbii 2980 |
. . . . . . . . . . . . . . . . 17
Poly deg deg Poly deg
deg
Poly deg deg Poly deg
deg |
85 | 75, 84 | sylib 208 |
. . . . . . . . . . . . . . . 16
Poly
Poly deg deg Poly deg
deg deg deg Poly deg deg
Poly
deg
deg |
86 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
coeff coeff |
87 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
coeff coeff |
88 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
deg deg |
89 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
deg deg |
90 | 61, 62, 63, 64, 65, 66, 67, 42, 68, 69, 70, 71, 74, 85, 86, 87, 88, 89 | plydivlem4 24051 |
. . . . . . . . . . . . . . 15
Poly
Poly deg deg Poly deg
deg deg deg Poly deg
deg |
91 | 90 | exp32 631 |
. . . . . . . . . . . . . 14
Poly
Poly deg deg Poly deg
deg deg deg Poly
deg
deg |
92 | 91 | ralrimdva 2969 |
. . . . . . . . . . . . 13
Poly deg deg Poly deg
deg Poly deg deg Poly deg
deg |
93 | 59, 92 | syl5bi 232 |
. . . . . . . . . . . 12
Poly deg deg Poly deg
deg Poly deg deg Poly deg
deg |
94 | 93 | ancld 576 |
. . . . . . . . . . 11
Poly deg deg Poly deg
deg Poly deg deg
Poly
deg
deg Poly deg deg Poly
deg
deg |
95 | | dgrcl 23989 |
. . . . . . . . . . . . . . . . . . . . . 22
Poly
deg |
96 | 95 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
Poly
deg |
97 | 96 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . . 20
Poly
deg |
98 | 5 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
Poly
Poly |
99 | 98, 6 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
Poly
deg |
100 | 99 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . . 20
Poly
deg |
101 | 97, 100 | zsubcld 11487 |
. . . . . . . . . . . . . . . . . . 19
Poly
deg deg |
102 | | nn0z 11400 |
. . . . . . . . . . . . . . . . . . . 20
|
103 | 102 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . 19
Poly
|
104 | | zleltp1 11428 |
. . . . . . . . . . . . . . . . . . 19
deg deg deg deg deg deg |
105 | 101, 103,
104 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
Poly
deg deg
deg deg |
106 | 101 | zred 11482 |
. . . . . . . . . . . . . . . . . . 19
Poly
deg deg |
107 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . 20
|
108 | 107 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . 19
Poly
|
109 | 106, 108 | leloed 10180 |
. . . . . . . . . . . . . . . . . 18
Poly
deg deg
deg deg
deg deg |
110 | 105, 109 | bitr3d 270 |
. . . . . . . . . . . . . . . . 17
Poly
deg deg
deg deg
deg deg |
111 | 110 | orbi2d 738 |
. . . . . . . . . . . . . . . 16
Poly
deg deg
deg deg deg deg |
112 | | pm5.63 959 |
. . . . . . . . . . . . . . . . . . . 20
deg deg
deg deg |
113 | | df-ne 2795 |
. . . . . . . . . . . . . . . . . . . . . 22
|
114 | 113 | anbi1i 731 |
. . . . . . . . . . . . . . . . . . . . 21
deg deg
deg deg |
115 | 114 | orbi2i 541 |
. . . . . . . . . . . . . . . . . . . 20
deg deg
deg deg |
116 | 112, 115 | bitr4i 267 |
. . . . . . . . . . . . . . . . . . 19
deg deg
deg deg |
117 | 116 | orbi2i 541 |
. . . . . . . . . . . . . . . . . 18
deg deg deg deg
deg deg
deg deg |
118 | | or12 545 |
. . . . . . . . . . . . . . . . . 18
deg deg deg deg deg deg deg deg |
119 | | or12 545 |
. . . . . . . . . . . . . . . . . 18
deg deg deg deg deg deg deg deg |
120 | 117, 118,
119 | 3bitr4i 292 |
. . . . . . . . . . . . . . . . 17
deg deg deg deg deg deg deg deg |
121 | | orass 546 |
. . . . . . . . . . . . . . . . 17
deg deg deg deg
deg deg deg deg |
122 | 120, 121 | bitr4i 267 |
. . . . . . . . . . . . . . . 16
deg deg deg deg deg deg deg deg |
123 | 111, 122 | syl6bb 276 |
. . . . . . . . . . . . . . 15
Poly
deg deg
deg deg deg deg |
124 | 123 | imbi1d 331 |
. . . . . . . . . . . . . 14
Poly
deg deg
Poly
deg
deg deg deg deg deg
Poly
deg
deg |
125 | | jaob 822 |
. . . . . . . . . . . . . 14
deg deg
deg deg
Poly
deg
deg deg deg Poly deg
deg deg deg Poly
deg
deg |
126 | 124, 125 | syl6bb 276 |
. . . . . . . . . . . . 13
Poly
deg deg
Poly
deg
deg deg deg Poly deg
deg deg deg Poly
deg
deg |
127 | 126 | ralbidva 2985 |
. . . . . . . . . . . 12
Poly deg deg Poly deg
deg
Poly deg deg
Poly
deg
deg deg deg Poly
deg
deg |
128 | | r19.26 3064 |
. . . . . . . . . . . 12
Poly deg deg Poly deg
deg deg deg Poly
deg
deg Poly deg deg
Poly
deg
deg Poly deg deg Poly
deg
deg |
129 | 127, 128 | syl6bb 276 |
. . . . . . . . . . 11
Poly deg deg Poly deg
deg Poly deg deg
Poly
deg
deg Poly deg deg Poly
deg
deg |
130 | 94, 129 | sylibrd 249 |
. . . . . . . . . 10
Poly deg deg Poly deg
deg Poly deg deg Poly deg
deg |
131 | 130 | expcom 451 |
. . . . . . . . 9
Poly deg deg
Poly
deg
deg Poly deg deg Poly deg
deg |
132 | 131 | a2d 29 |
. . . . . . . 8
Poly deg deg Poly deg
deg
Poly deg deg Poly deg
deg |
133 | 19, 24, 29, 24, 46, 132 | nn0ind 11472 |
. . . . . . 7
Poly deg deg Poly deg
deg |
134 | 14, 133 | syl 17 |
. . . . . 6
Poly deg deg Poly deg
deg |
135 | 134 | impcom 446 |
. . . . 5
Poly deg deg
Poly
deg
deg |
136 | | eqeq1 2626 |
. . . . . . . 8
|
137 | | fveq2 6191 |
. . . . . . . . . 10
deg deg |
138 | 137 | oveq1d 6665 |
. . . . . . . . 9
deg deg deg deg |
139 | 138 | breq1d 4663 |
. . . . . . . 8
deg deg deg deg |
140 | 136, 139 | orbi12d 746 |
. . . . . . 7
deg deg
deg deg |
141 | | oveq1 6657 |
. . . . . . . . . . 11
|
142 | | plydiv.r |
. . . . . . . . . . 11
|
143 | 141, 142 | syl6eqr 2674 |
. . . . . . . . . 10
|
144 | 143 | eqeq1d 2624 |
. . . . . . . . 9
|
145 | 143 | fveq2d 6195 |
. . . . . . . . . 10
deg
deg |
146 | 145 | breq1d 4663 |
. . . . . . . . 9
deg
deg deg deg |
147 | 144, 146 | orbi12d 746 |
. . . . . . . 8
deg
deg
deg deg |
148 | 147 | rexbidv 3052 |
. . . . . . 7
Poly
deg
deg
Poly deg deg |
149 | 140, 148 | imbi12d 334 |
. . . . . 6
deg deg
Poly
deg
deg deg deg
Poly deg deg |
150 | 149 | rspcv 3305 |
. . . . 5
Poly
Poly deg deg Poly deg
deg deg deg Poly deg deg |
151 | 13, 135, 150 | sylc 65 |
. . . 4
deg deg Poly deg deg |
152 | 12, 151 | syl5 34 |
. . 3
deg deg
Poly deg deg |
153 | 152 | rexlimdva 3031 |
. 2
deg deg
Poly deg deg |
154 | 11, 153 | mpd 15 |
1
Poly deg deg |