Step | Hyp | Ref
| Expression |
1 | | plyssc 23956 |
. . 3
Poly Poly |
2 | | dgrco.3 |
. . 3
Poly |
3 | 1, 2 | sseldi 3601 |
. 2
Poly |
4 | | dgrco.1 |
. . . 4
deg |
5 | | dgrcl 23989 |
. . . . 5
Poly
deg |
6 | 2, 5 | syl 17 |
. . . 4
deg |
7 | 4, 6 | syl5eqel 2705 |
. . 3
|
8 | | breq2 4657 |
. . . . . . 7
deg deg |
9 | 8 | imbi1d 331 |
. . . . . 6
deg
deg deg deg deg deg |
10 | 9 | ralbidv 2986 |
. . . . 5
Polydeg deg deg
Polydeg
deg deg |
11 | 10 | imbi2d 330 |
. . . 4
Polydeg
deg deg
Polydeg
deg deg |
12 | | breq2 4657 |
. . . . . . 7
deg deg |
13 | 12 | imbi1d 331 |
. . . . . 6
deg
deg deg deg deg deg |
14 | 13 | ralbidv 2986 |
. . . . 5
Polydeg deg deg
Polydeg
deg deg |
15 | 14 | imbi2d 330 |
. . . 4
Polydeg
deg deg
Polydeg
deg deg |
16 | | breq2 4657 |
. . . . . . 7
deg deg |
17 | 16 | imbi1d 331 |
. . . . . 6
deg
deg deg deg deg deg |
18 | 17 | ralbidv 2986 |
. . . . 5
Polydeg deg deg
Polydeg
deg deg |
19 | 18 | imbi2d 330 |
. . . 4
Polydeg
deg deg
Polydeg
deg deg |
20 | | breq2 4657 |
. . . . . . 7
deg deg |
21 | 20 | imbi1d 331 |
. . . . . 6
deg
deg deg deg deg deg |
22 | 21 | ralbidv 2986 |
. . . . 5
Polydeg deg deg
Polydeg
deg deg |
23 | 22 | imbi2d 330 |
. . . 4
Polydeg
deg deg
Polydeg deg deg |
24 | | dgrco.2 |
. . . . . . . . . . . 12
deg |
25 | | dgrco.4 |
. . . . . . . . . . . . 13
Poly |
26 | | dgrcl 23989 |
. . . . . . . . . . . . 13
Poly
deg |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . 12
deg |
28 | 24, 27 | syl5eqel 2705 |
. . . . . . . . . . 11
|
29 | 28 | nn0cnd 11353 |
. . . . . . . . . 10
|
30 | 29 | adantr 481 |
. . . . . . . . 9
Poly deg
|
31 | 30 | mul02d 10234 |
. . . . . . . 8
Poly deg |
32 | | simprr 796 |
. . . . . . . . . 10
Poly deg deg |
33 | | dgrcl 23989 |
. . . . . . . . . . . 12
Poly deg |
34 | 33 | ad2antrl 764 |
. . . . . . . . . . 11
Poly deg deg |
35 | 34 | nn0ge0d 11354 |
. . . . . . . . . 10
Poly deg
deg |
36 | 34 | nn0red 11352 |
. . . . . . . . . . 11
Poly deg deg |
37 | | 0re 10040 |
. . . . . . . . . . 11
|
38 | | letri3 10123 |
. . . . . . . . . . 11
deg deg
deg
deg |
39 | 36, 37, 38 | sylancl 694 |
. . . . . . . . . 10
Poly deg deg deg deg |
40 | 32, 35, 39 | mpbir2and 957 |
. . . . . . . . 9
Poly deg deg |
41 | 40 | oveq1d 6665 |
. . . . . . . 8
Poly deg deg |
42 | 31, 41, 40 | 3eqtr4d 2666 |
. . . . . . 7
Poly deg deg deg |
43 | | fconstmpt 5163 |
. . . . . . . . 9
|
44 | | 0dgrb 24002 |
. . . . . . . . . . 11
Poly deg |
45 | 44 | ad2antrl 764 |
. . . . . . . . . 10
Poly deg deg |
46 | 40, 45 | mpbid 222 |
. . . . . . . . 9
Poly deg |
47 | 25 | adantr 481 |
. . . . . . . . . . . 12
Poly deg
Poly |
48 | | plyf 23954 |
. . . . . . . . . . . 12
Poly
|
49 | 47, 48 | syl 17 |
. . . . . . . . . . 11
Poly deg |
50 | 49 | ffvelrnda 6359 |
. . . . . . . . . 10
Poly
deg |
51 | 49 | feqmptd 6249 |
. . . . . . . . . 10
Poly deg
|
52 | | fconstmpt 5163 |
. . . . . . . . . . 11
|
53 | 46, 52 | syl6eq 2672 |
. . . . . . . . . 10
Poly deg |
54 | | eqidd 2623 |
. . . . . . . . . 10
|
55 | 50, 51, 53, 54 | fmptco 6396 |
. . . . . . . . 9
Poly deg |
56 | 43, 46, 55 | 3eqtr4a 2682 |
. . . . . . . 8
Poly deg |
57 | 56 | fveq2d 6195 |
. . . . . . 7
Poly deg deg deg |
58 | 42, 57 | eqtr2d 2657 |
. . . . . 6
Poly deg deg deg |
59 | 58 | expr 643 |
. . . . 5
Poly deg deg deg |
60 | 59 | ralrimiva 2966 |
. . . 4
Polydeg
deg deg |
61 | | fveq2 6191 |
. . . . . . . . . 10
deg deg |
62 | 61 | breq1d 4663 |
. . . . . . . . 9
deg deg |
63 | | coeq1 5279 |
. . . . . . . . . . 11
|
64 | 63 | fveq2d 6195 |
. . . . . . . . . 10
deg deg |
65 | 61 | oveq1d 6665 |
. . . . . . . . . 10
deg deg |
66 | 64, 65 | eqeq12d 2637 |
. . . . . . . . 9
deg deg deg deg |
67 | 62, 66 | imbi12d 334 |
. . . . . . . 8
deg
deg deg deg deg deg |
68 | 67 | cbvralv 3171 |
. . . . . . 7
Polydeg deg deg Polydeg
deg deg |
69 | 33 | ad2antrl 764 |
. . . . . . . . . . . 12
Poly
Polydeg
deg deg deg |
70 | 69 | nn0red 11352 |
. . . . . . . . . . 11
Poly
Polydeg
deg deg deg |
71 | | nn0p1nn 11332 |
. . . . . . . . . . . . 13
|
72 | 71 | ad2antlr 763 |
. . . . . . . . . . . 12
Poly
Polydeg
deg deg |
73 | 72 | nnred 11035 |
. . . . . . . . . . 11
Poly
Polydeg
deg deg |
74 | 70, 73 | leloed 10180 |
. . . . . . . . . 10
Poly
Polydeg
deg deg deg
deg deg |
75 | | simplr 792 |
. . . . . . . . . . . . 13
Poly
Polydeg
deg deg |
76 | | nn0leltp1 11436 |
. . . . . . . . . . . . 13
deg deg deg |
77 | 69, 75, 76 | syl2anc 693 |
. . . . . . . . . . . 12
Poly
Polydeg
deg deg deg
deg
|
78 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
deg deg |
79 | 78 | breq1d 4663 |
. . . . . . . . . . . . . . 15
deg deg |
80 | | coeq1 5279 |
. . . . . . . . . . . . . . . . 17
|
81 | 80 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
deg deg |
82 | 78 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
deg deg |
83 | 81, 82 | eqeq12d 2637 |
. . . . . . . . . . . . . . 15
deg deg deg deg |
84 | 79, 83 | imbi12d 334 |
. . . . . . . . . . . . . 14
deg
deg deg deg deg deg |
85 | 84 | rspcva 3307 |
. . . . . . . . . . . . 13
Poly
Polydeg
deg deg deg
deg deg |
86 | 85 | adantl 482 |
. . . . . . . . . . . 12
Poly
Polydeg
deg deg deg
deg deg |
87 | 77, 86 | sylbird 250 |
. . . . . . . . . . 11
Poly
Polydeg
deg deg deg
deg deg |
88 | | eqid 2622 |
. . . . . . . . . . . . 13
deg deg |
89 | | simprll 802 |
. . . . . . . . . . . . 13
Poly
Polydeg deg deg deg Poly |
90 | 1, 25 | sseldi 3601 |
. . . . . . . . . . . . . 14
Poly |
91 | 90 | ad2antrr 762 |
. . . . . . . . . . . . 13
Poly
Polydeg deg deg deg Poly |
92 | | eqid 2622 |
. . . . . . . . . . . . 13
coeff coeff |
93 | | simplr 792 |
. . . . . . . . . . . . 13
Poly
Polydeg deg deg deg |
94 | | simprr 796 |
. . . . . . . . . . . . 13
Poly
Polydeg deg deg deg deg |
95 | | simprlr 803 |
. . . . . . . . . . . . . 14
Poly
Polydeg deg deg deg Polydeg
deg deg |
96 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
deg deg |
97 | 96 | breq1d 4663 |
. . . . . . . . . . . . . . . 16
deg deg |
98 | | coeq1 5279 |
. . . . . . . . . . . . . . . . . 18
|
99 | 98 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
deg deg |
100 | 96 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
deg deg |
101 | 99, 100 | eqeq12d 2637 |
. . . . . . . . . . . . . . . 16
deg deg deg deg |
102 | 97, 101 | imbi12d 334 |
. . . . . . . . . . . . . . 15
deg
deg deg deg deg deg |
103 | 102 | cbvralv 3171 |
. . . . . . . . . . . . . 14
Polydeg deg deg Polydeg
deg deg |
104 | 95, 103 | sylib 208 |
. . . . . . . . . . . . 13
Poly
Polydeg deg deg deg Polydeg
deg deg |
105 | 88, 24, 89, 91, 92, 93, 94, 104 | dgrcolem2 24030 |
. . . . . . . . . . . 12
Poly
Polydeg deg deg deg deg deg |
106 | 105 | expr 643 |
. . . . . . . . . . 11
Poly
Polydeg
deg deg deg deg deg |
107 | 87, 106 | jaod 395 |
. . . . . . . . . 10
Poly
Polydeg
deg deg deg deg deg deg |
108 | 74, 107 | sylbid 230 |
. . . . . . . . 9
Poly
Polydeg
deg deg deg
deg deg |
109 | 108 | expr 643 |
. . . . . . . 8
Poly
Polydeg deg deg
deg deg deg |
110 | 109 | ralrimdva 2969 |
. . . . . . 7
Polydeg deg deg
Polydeg
deg deg |
111 | 68, 110 | syl5bi 232 |
. . . . . 6
Polydeg deg deg
Polydeg
deg deg |
112 | 111 | expcom 451 |
. . . . 5
Polydeg
deg deg
Polydeg
deg deg |
113 | 112 | a2d 29 |
. . . 4
Polydeg
deg deg Polydeg deg deg |
114 | 11, 15, 19, 23, 60, 113 | nn0ind 11472 |
. . 3
Polydeg deg deg |
115 | 7, 114 | mpcom 38 |
. 2
Polydeg deg deg |
116 | 7 | nn0red 11352 |
. . 3
|
117 | 116 | leidd 10594 |
. 2
|
118 | | fveq2 6191 |
. . . . . 6
deg deg |
119 | 118, 4 | syl6eqr 2674 |
. . . . 5
deg |
120 | 119 | breq1d 4663 |
. . . 4
deg
|
121 | | coeq1 5279 |
. . . . . 6
|
122 | 121 | fveq2d 6195 |
. . . . 5
deg deg |
123 | 119 | oveq1d 6665 |
. . . . 5
deg |
124 | 122, 123 | eqeq12d 2637 |
. . . 4
deg deg deg |
125 | 120, 124 | imbi12d 334 |
. . 3
deg
deg deg deg
|
126 | 125 | rspcv 3305 |
. 2
Poly Polydeg
deg deg
deg
|
127 | 3, 115, 117, 126 | syl3c 66 |
1
deg |