Step | Hyp | Ref
| Expression |
1 | | fta1.3 |
. . . . . . . . . 10
Poly |
2 | | eldifsn 4317 |
. . . . . . . . . 10
Poly
Poly
|
3 | 1, 2 | sylib 208 |
. . . . . . . . 9
Poly |
4 | 3 | simpld 475 |
. . . . . . . 8
Poly |
5 | | fta1.5 |
. . . . . . . . . 10
|
6 | | plyf 23954 |
. . . . . . . . . . 11
Poly |
7 | | ffn 6045 |
. . . . . . . . . . 11
|
8 | | fniniseg 6338 |
. . . . . . . . . . 11
|
9 | 4, 6, 7, 8 | 4syl 19 |
. . . . . . . . . 10
|
10 | 5, 9 | mpbid 222 |
. . . . . . . . 9
|
11 | 10 | simpld 475 |
. . . . . . . 8
|
12 | 10 | simprd 479 |
. . . . . . . 8
|
13 | | eqid 2622 |
. . . . . . . . 9
|
14 | 13 | facth 24061 |
. . . . . . . 8
Poly
quot |
15 | 4, 11, 12, 14 | syl3anc 1326 |
. . . . . . 7
quot |
16 | 15 | cnveqd 5298 |
. . . . . 6
quot |
17 | 16 | imaeq1d 5465 |
. . . . 5
quot |
18 | | cnex 10017 |
. . . . . . 7
|
19 | 18 | a1i 11 |
. . . . . 6
|
20 | | ssid 3624 |
. . . . . . . . 9
|
21 | | ax-1cn 9994 |
. . . . . . . . 9
|
22 | | plyid 23965 |
. . . . . . . . 9
Poly |
23 | 20, 21, 22 | mp2an 708 |
. . . . . . . 8
Poly |
24 | | plyconst 23962 |
. . . . . . . . 9
Poly |
25 | 20, 11, 24 | sylancr 695 |
. . . . . . . 8
Poly |
26 | | plysubcl 23978 |
. . . . . . . 8
Poly Poly Poly |
27 | 23, 25, 26 | sylancr 695 |
. . . . . . 7
Poly |
28 | | plyf 23954 |
. . . . . . 7
Poly |
29 | 27, 28 | syl 17 |
. . . . . 6
|
30 | 13 | plyremlem 24059 |
. . . . . . . . . . . 12
Poly deg |
31 | 11, 30 | syl 17 |
. . . . . . . . . . 11
Poly deg |
32 | 31 | simp2d 1074 |
. . . . . . . . . 10
deg |
33 | | ax-1ne0 10005 |
. . . . . . . . . . 11
|
34 | 33 | a1i 11 |
. . . . . . . . . 10
|
35 | 32, 34 | eqnetrd 2861 |
. . . . . . . . 9
deg |
36 | | fveq2 6191 |
. . . . . . . . . . 11
deg deg |
37 | | dgr0 24018 |
. . . . . . . . . . 11
deg |
38 | 36, 37 | syl6eq 2672 |
. . . . . . . . . 10
deg |
39 | 38 | necon3i 2826 |
. . . . . . . . 9
deg
|
40 | 35, 39 | syl 17 |
. . . . . . . 8
|
41 | | quotcl2 24057 |
. . . . . . . 8
Poly
Poly quot Poly |
42 | 4, 27, 40, 41 | syl3anc 1326 |
. . . . . . 7
quot
Poly |
43 | | plyf 23954 |
. . . . . . 7
quot Poly quot
|
44 | 42, 43 | syl 17 |
. . . . . 6
quot
|
45 | | ofmulrt 24037 |
. . . . . 6
quot quot quot
|
46 | 19, 29, 44, 45 | syl3anc 1326 |
. . . . 5
quot quot |
47 | 31 | simp3d 1075 |
. . . . . 6
|
48 | 47 | uneq1d 3766 |
. . . . 5
quot
quot |
49 | 17, 46, 48 | 3eqtrd 2660 |
. . . 4
quot |
50 | | fta1.1 |
. . . 4
|
51 | | uncom 3757 |
. . . 4
quot quot |
52 | 49, 50, 51 | 3eqtr4g 2681 |
. . 3
quot |
53 | 3 | simprd 479 |
. . . . . . . . 9
|
54 | 15 | eqcomd 2628 |
. . . . . . . . 9
quot |
55 | | 0cnd 10033 |
. . . . . . . . . . 11
|
56 | | mul01 10215 |
. . . . . . . . . . . 12
|
57 | 56 | adantl 482 |
. . . . . . . . . . 11
|
58 | 19, 29, 55, 55, 57 | caofid1 6927 |
. . . . . . . . . 10
|
59 | | df-0p 23437 |
. . . . . . . . . . 11
|
60 | 59 | oveq2i 6661 |
. . . . . . . . . 10
|
61 | 58, 60, 59 | 3eqtr4g 2681 |
. . . . . . . . 9
|
62 | 53, 54, 61 | 3netr4d 2871 |
. . . . . . . 8
quot |
63 | | oveq2 6658 |
. . . . . . . . 9
quot quot |
64 | 63 | necon3i 2826 |
. . . . . . . 8
quot quot |
65 | 62, 64 | syl 17 |
. . . . . . 7
quot
|
66 | | eldifsn 4317 |
. . . . . . 7
quot Poly
quot Poly quot
|
67 | 42, 65, 66 | sylanbrc 698 |
. . . . . 6
quot
Poly
|
68 | | fta1.6 |
. . . . . 6
Poly deg deg |
69 | 21 | a1i 11 |
. . . . . . 7
|
70 | | dgrcl 23989 |
. . . . . . . . 9
quot Poly deg quot |
71 | 42, 70 | syl 17 |
. . . . . . . 8
deg quot |
72 | 71 | nn0cnd 11353 |
. . . . . . 7
deg quot |
73 | | fta1.2 |
. . . . . . . 8
|
74 | 73 | nn0cnd 11353 |
. . . . . . 7
|
75 | | addcom 10222 |
. . . . . . . . 9
|
76 | 21, 74, 75 | sylancr 695 |
. . . . . . . 8
|
77 | 15 | fveq2d 6195 |
. . . . . . . . 9
deg deg quot |
78 | | fta1.4 |
. . . . . . . . 9
deg |
79 | | eqid 2622 |
. . . . . . . . . . 11
deg deg |
80 | | eqid 2622 |
. . . . . . . . . . 11
deg
quot deg quot |
81 | 79, 80 | dgrmul 24026 |
. . . . . . . . . 10
Poly quot Poly quot
deg quot deg deg
quot |
82 | 27, 40, 42, 65, 81 | syl22anc 1327 |
. . . . . . . . 9
deg quot deg deg quot |
83 | 77, 78, 82 | 3eqtr3d 2664 |
. . . . . . . 8
deg deg quot |
84 | 32 | oveq1d 6665 |
. . . . . . . 8
deg deg
quot deg quot |
85 | 76, 83, 84 | 3eqtrrd 2661 |
. . . . . . 7
deg quot |
86 | 69, 72, 74, 85 | addcanad 10241 |
. . . . . 6
deg quot |
87 | | fveq2 6191 |
. . . . . . . . 9
quot
deg deg
quot |
88 | 87 | eqeq1d 2624 |
. . . . . . . 8
quot
deg deg quot |
89 | | cnveq 5296 |
. . . . . . . . . . 11
quot
quot |
90 | 89 | imaeq1d 5465 |
. . . . . . . . . 10
quot
quot
|
91 | 90 | eleq1d 2686 |
. . . . . . . . 9
quot
quot |
92 | 90 | fveq2d 6195 |
. . . . . . . . . 10
quot
quot |
93 | 92, 87 | breq12d 4666 |
. . . . . . . . 9
quot
deg
quot deg quot |
94 | 91, 93 | anbi12d 747 |
. . . . . . . 8
quot
deg
quot quot deg quot |
95 | 88, 94 | imbi12d 334 |
. . . . . . 7
quot
deg
deg
deg quot
quot quot
deg quot |
96 | 95 | rspcv 3305 |
. . . . . 6
quot Poly
Poly deg deg deg quot quot quot
deg quot |
97 | 67, 68, 86, 96 | syl3c 66 |
. . . . 5
quot quot
deg quot |
98 | 97 | simpld 475 |
. . . 4
quot |
99 | | snfi 8038 |
. . . 4
|
100 | | unfi 8227 |
. . . 4
quot
quot
|
101 | 98, 99, 100 | sylancl 694 |
. . 3
quot |
102 | 52, 101 | eqeltrd 2701 |
. 2
|
103 | 52 | fveq2d 6195 |
. . 3
quot |
104 | | hashcl 13147 |
. . . . . 6
quot quot |
105 | 101, 104 | syl 17 |
. . . . 5
quot |
106 | 105 | nn0red 11352 |
. . . 4
quot |
107 | | hashcl 13147 |
. . . . . . 7
quot quot |
108 | 98, 107 | syl 17 |
. . . . . 6
quot |
109 | 108 | nn0red 11352 |
. . . . 5
quot |
110 | | peano2re 10209 |
. . . . 5
quot quot |
111 | 109, 110 | syl 17 |
. . . 4
quot |
112 | | dgrcl 23989 |
. . . . . 6
Poly deg |
113 | 4, 112 | syl 17 |
. . . . 5
deg |
114 | 113 | nn0red 11352 |
. . . 4
deg |
115 | | hashun2 13172 |
. . . . . 6
quot
quot quot
|
116 | 98, 99, 115 | sylancl 694 |
. . . . 5
quot quot
|
117 | | hashsng 13159 |
. . . . . . 7
|
118 | 11, 117 | syl 17 |
. . . . . 6
|
119 | 118 | oveq2d 6666 |
. . . . 5
quot quot |
120 | 116, 119 | breqtrd 4679 |
. . . 4
quot quot
|
121 | 73 | nn0red 11352 |
. . . . . 6
|
122 | | 1red 10055 |
. . . . . 6
|
123 | 97 | simprd 479 |
. . . . . . 7
quot deg quot |
124 | 123, 86 | breqtrd 4679 |
. . . . . 6
quot |
125 | 109, 121,
122, 124 | leadd1dd 10641 |
. . . . 5
quot
|
126 | 125, 78 | breqtrrd 4681 |
. . . 4
quot deg |
127 | 106, 111,
114, 120, 126 | letrd 10194 |
. . 3
quot deg |
128 | 103, 127 | eqbrtrd 4675 |
. 2
deg |
129 | 102, 128 | jca 554 |
1
deg |