Step | Hyp | Ref
| Expression |
1 | | qsscn 11799 |
. . . . . 6
|
2 | | eldifi 3732 |
. . . . . . . . . 10
Poly
Poly |
3 | 2 | ad2antlr 763 |
. . . . . . . . 9
Poly deg degAA
Poly |
4 | | zssq 11795 |
. . . . . . . . . 10
|
5 | | 0z 11388 |
. . . . . . . . . 10
|
6 | 4, 5 | sselii 3600 |
. . . . . . . . 9
|
7 | | eqid 2622 |
. . . . . . . . . 10
coeff coeff |
8 | 7 | coef2 23987 |
. . . . . . . . 9
Poly
coeff |
9 | 3, 6, 8 | sylancl 694 |
. . . . . . . 8
Poly deg degAA
coeff |
10 | | dgrcl 23989 |
. . . . . . . . 9
Poly deg |
11 | 3, 10 | syl 17 |
. . . . . . . 8
Poly deg degAA
deg |
12 | 9, 11 | ffvelrnd 6360 |
. . . . . . 7
Poly deg degAA
coeffdeg |
13 | | eldifsni 4320 |
. . . . . . . . 9
Poly
|
14 | 13 | ad2antlr 763 |
. . . . . . . 8
Poly deg degAA
|
15 | | eqid 2622 |
. . . . . . . . . . 11
deg deg |
16 | 15, 7 | dgreq0 24021 |
. . . . . . . . . 10
Poly
coeffdeg |
17 | 16 | necon3bid 2838 |
. . . . . . . . 9
Poly
coeffdeg |
18 | 3, 17 | syl 17 |
. . . . . . . 8
Poly deg degAA
coeffdeg |
19 | 14, 18 | mpbid 222 |
. . . . . . 7
Poly deg degAA
coeffdeg |
20 | | qreccl 11808 |
. . . . . . 7
coeffdeg coeffdeg
coeffdeg |
21 | 12, 19, 20 | syl2anc 693 |
. . . . . 6
Poly deg degAA
coeffdeg |
22 | | plyconst 23962 |
. . . . . 6
coeffdeg coeffdeg Poly |
23 | 1, 21, 22 | sylancr 695 |
. . . . 5
Poly deg degAA
coeffdeg Poly |
24 | | simpl 473 |
. . . . . 6
coeffdeg Poly Poly coeffdeg Poly |
25 | | simpr 477 |
. . . . . 6
coeffdeg Poly Poly Poly |
26 | | qaddcl 11804 |
. . . . . . 7
|
27 | 26 | adantl 482 |
. . . . . 6
coeffdeg Poly
Poly
|
28 | | qmulcl 11806 |
. . . . . . 7
|
29 | 28 | adantl 482 |
. . . . . 6
coeffdeg Poly
Poly
|
30 | 24, 25, 27, 29 | plymul 23974 |
. . . . 5
coeffdeg Poly Poly coeffdeg Poly |
31 | 23, 3, 30 | syl2anc 693 |
. . . 4
Poly deg degAA
coeffdeg Poly |
32 | 7 | coef3 23988 |
. . . . . . . . 9
Poly coeff |
33 | 3, 32 | syl 17 |
. . . . . . . 8
Poly deg degAA
coeff |
34 | 33, 11 | ffvelrnd 6360 |
. . . . . . 7
Poly deg degAA
coeffdeg |
35 | 34, 19 | reccld 10794 |
. . . . . 6
Poly deg degAA
coeffdeg |
36 | 34, 19 | recne0d 10795 |
. . . . . 6
Poly deg degAA
coeffdeg |
37 | | dgrmulc 24027 |
. . . . . 6
coeffdeg coeffdeg
Poly deg coeffdeg deg |
38 | 35, 36, 3, 37 | syl3anc 1326 |
. . . . 5
Poly deg degAA
deg coeffdeg deg |
39 | | simprl 794 |
. . . . 5
Poly deg degAA
deg degAA |
40 | 38, 39 | eqtrd 2656 |
. . . 4
Poly deg degAA
deg coeffdeg degAA |
41 | | aacn 24072 |
. . . . . . 7
|
42 | 41 | ad2antrr 762 |
. . . . . 6
Poly deg degAA
|
43 | | ovex 6678 |
. . . . . . . 8
coeffdeg |
44 | | fnconstg 6093 |
. . . . . . . 8
coeffdeg coeffdeg |
45 | 43, 44 | mp1i 13 |
. . . . . . 7
Poly deg degAA
coeffdeg |
46 | | plyf 23954 |
. . . . . . . 8
Poly |
47 | | ffn 6045 |
. . . . . . . 8
|
48 | 3, 46, 47 | 3syl 18 |
. . . . . . 7
Poly deg degAA
|
49 | | cnex 10017 |
. . . . . . . 8
|
50 | 49 | a1i 11 |
. . . . . . 7
Poly deg degAA
|
51 | | inidm 3822 |
. . . . . . 7
|
52 | 43 | fvconst2 6469 |
. . . . . . . 8
coeffdeg coeffdeg |
53 | 52 | adantl 482 |
. . . . . . 7
Poly deg degAA coeffdeg coeffdeg |
54 | | simplrr 801 |
. . . . . . 7
Poly deg degAA |
55 | 45, 48, 50, 50, 51, 53, 54 | ofval 6906 |
. . . . . 6
Poly deg degAA coeffdeg coeffdeg |
56 | 42, 55 | mpdan 702 |
. . . . 5
Poly deg degAA
coeffdeg coeffdeg |
57 | 35 | mul01d 10235 |
. . . . 5
Poly deg degAA
coeffdeg |
58 | 56, 57 | eqtrd 2656 |
. . . 4
Poly deg degAA
coeffdeg |
59 | | coemulc 24011 |
. . . . . . 7
coeffdeg Poly coeff coeffdeg coeffdeg coeff |
60 | 35, 3, 59 | syl2anc 693 |
. . . . . 6
Poly deg degAA
coeff coeffdeg coeffdeg coeff |
61 | 60 | fveq1d 6193 |
. . . . 5
Poly deg degAA
coeff coeffdeg degAA coeffdeg coeffdegAA |
62 | | dgraacl 37716 |
. . . . . . . 8
degAA |
63 | 62 | ad2antrr 762 |
. . . . . . 7
Poly deg degAA
degAA |
64 | 63 | nnnn0d 11351 |
. . . . . 6
Poly deg degAA
degAA |
65 | | fnconstg 6093 |
. . . . . . . 8
coeffdeg coeffdeg |
66 | 43, 65 | mp1i 13 |
. . . . . . 7
Poly deg degAA
coeffdeg |
67 | | ffn 6045 |
. . . . . . . 8
coeff coeff |
68 | 33, 67 | syl 17 |
. . . . . . 7
Poly deg degAA
coeff |
69 | | nn0ex 11298 |
. . . . . . . 8
|
70 | 69 | a1i 11 |
. . . . . . 7
Poly deg degAA
|
71 | | inidm 3822 |
. . . . . . 7
|
72 | 43 | fvconst2 6469 |
. . . . . . . 8
degAA coeffdegdegAA coeffdeg |
73 | 72 | adantl 482 |
. . . . . . 7
Poly deg degAA degAA coeffdegdegAA coeffdeg |
74 | | simplrl 800 |
. . . . . . . . 9
Poly deg degAA degAA deg degAA |
75 | 74 | eqcomd 2628 |
. . . . . . . 8
Poly deg degAA degAA degAA deg |
76 | 75 | fveq2d 6195 |
. . . . . . 7
Poly deg degAA degAA coeffdegAA coeffdeg |
77 | 66, 68, 70, 70, 71, 73, 76 | ofval 6906 |
. . . . . 6
Poly deg degAA degAA coeffdeg coeffdegAA coeffdeg coeffdeg |
78 | 64, 77 | mpdan 702 |
. . . . 5
Poly deg degAA
coeffdeg coeffdegAA coeffdeg coeffdeg |
79 | 34, 19 | recid2d 10797 |
. . . . 5
Poly deg degAA
coeffdeg coeffdeg |
80 | 61, 78, 79 | 3eqtrd 2660 |
. . . 4
Poly deg degAA
coeff coeffdeg degAA |
81 | | fveq2 6191 |
. . . . . . 7
coeffdeg deg deg coeffdeg |
82 | 81 | eqeq1d 2624 |
. . . . . 6
coeffdeg deg degAA deg coeffdeg degAA |
83 | | fveq1 6190 |
. . . . . . 7
coeffdeg coeffdeg |
84 | 83 | eqeq1d 2624 |
. . . . . 6
coeffdeg coeffdeg |
85 | | fveq2 6191 |
. . . . . . . 8
coeffdeg coeff coeff coeffdeg |
86 | 85 | fveq1d 6193 |
. . . . . . 7
coeffdeg coeffdegAA coeff coeffdeg degAA |
87 | 86 | eqeq1d 2624 |
. . . . . 6
coeffdeg coeffdegAA coeff coeffdeg degAA |
88 | 82, 84, 87 | 3anbi123d 1399 |
. . . . 5
coeffdeg deg degAA coeffdegAA
deg coeffdeg degAA coeffdeg coeff coeffdeg degAA |
89 | 88 | rspcev 3309 |
. . . 4
coeffdeg Poly deg coeffdeg degAA coeffdeg coeff coeffdeg degAA
Polydeg degAA coeffdegAA |
90 | 31, 40, 58, 80, 89 | syl13anc 1328 |
. . 3
Poly deg degAA
Polydeg degAA
coeffdegAA |
91 | | dgraalem 37715 |
. . . 4
degAA Poly deg degAA |
92 | 91 | simprd 479 |
. . 3
Poly deg degAA |
93 | 90, 92 | r19.29a 3078 |
. 2
Polydeg degAA
coeffdegAA |
94 | | simp2 1062 |
. . . . . . . . . . 11
deg degAA coeffdegAA
|
95 | | simp2 1062 |
. . . . . . . . . . 11
deg degAA coeffdegAA
|
96 | 94, 95 | anim12i 590 |
. . . . . . . . . 10
deg degAA
coeffdegAA deg degAA coeffdegAA |
97 | | plyf 23954 |
. . . . . . . . . . . . . . . 16
Poly |
98 | | ffn 6045 |
. . . . . . . . . . . . . . . 16
|
99 | 97, 98 | syl 17 |
. . . . . . . . . . . . . . 15
Poly |
100 | 99 | ad2antrr 762 |
. . . . . . . . . . . . . 14
Poly Poly
|
101 | 46, 47 | syl 17 |
. . . . . . . . . . . . . . 15
Poly |
102 | 101 | ad2antlr 763 |
. . . . . . . . . . . . . 14
Poly Poly
|
103 | 49 | a1i 11 |
. . . . . . . . . . . . . 14
Poly Poly
|
104 | | simplrl 800 |
. . . . . . . . . . . . . 14
Poly
Poly |
105 | | simplrr 801 |
. . . . . . . . . . . . . 14
Poly
Poly |
106 | 100, 102,
103, 103, 51, 104, 105 | ofval 6906 |
. . . . . . . . . . . . 13
Poly
Poly |
107 | 41, 106 | sylan2 491 |
. . . . . . . . . . . 12
Poly
Poly |
108 | | 0m0e0 11130 |
. . . . . . . . . . . 12
|
109 | 107, 108 | syl6eq 2672 |
. . . . . . . . . . 11
Poly
Poly |
110 | 109 | ex 450 |
. . . . . . . . . 10
Poly Poly
|
111 | 96, 110 | sylan2 491 |
. . . . . . . . 9
Poly Poly
deg degAA coeffdegAA deg degAA coeffdegAA |
112 | 111 | com12 32 |
. . . . . . . 8
Poly
Poly deg degAA coeffdegAA deg degAA coeffdegAA |
113 | 112 | impl 650 |
. . . . . . 7
Poly Poly deg degAA
coeffdegAA deg degAA coeffdegAA |
114 | | simpll 790 |
. . . . . . . 8
Poly Poly deg degAA
coeffdegAA deg degAA coeffdegAA
|
115 | | simpl 473 |
. . . . . . . . . 10
Poly
Poly
Poly |
116 | | simpr 477 |
. . . . . . . . . 10
Poly
Poly
Poly |
117 | 26 | adantl 482 |
. . . . . . . . . 10
Poly Poly
|
118 | 28 | adantl 482 |
. . . . . . . . . 10
Poly Poly
|
119 | | 1z 11407 |
. . . . . . . . . . . 12
|
120 | | zq 11794 |
. . . . . . . . . . . 12
|
121 | | qnegcl 11805 |
. . . . . . . . . . . 12
|
122 | 119, 120,
121 | mp2b 10 |
. . . . . . . . . . 11
|
123 | 122 | a1i 11 |
. . . . . . . . . 10
Poly
Poly
|
124 | 115, 116,
117, 118, 123 | plysub 23975 |
. . . . . . . . 9
Poly
Poly
Poly |
125 | 124 | ad2antlr 763 |
. . . . . . . 8
Poly Poly deg degAA
coeffdegAA deg degAA coeffdegAA Poly |
126 | | simplrl 800 |
. . . . . . . . . 10
Poly Poly deg degAA
coeffdegAA deg degAA coeffdegAA
Poly |
127 | | simplrr 801 |
. . . . . . . . . 10
Poly Poly deg degAA
coeffdegAA deg degAA coeffdegAA Poly |
128 | | simprr1 1109 |
. . . . . . . . . . 11
Poly Poly deg degAA
coeffdegAA deg degAA coeffdegAA deg degAA |
129 | | simprl1 1106 |
. . . . . . . . . . 11
Poly Poly deg degAA
coeffdegAA deg degAA coeffdegAA deg degAA |
130 | 128, 129 | eqtr4d 2659 |
. . . . . . . . . 10
Poly Poly deg degAA
coeffdegAA deg degAA coeffdegAA deg deg |
131 | 62 | ad2antrr 762 |
. . . . . . . . . . 11
Poly Poly deg degAA
coeffdegAA deg degAA coeffdegAA degAA |
132 | 129, 131 | eqeltrd 2701 |
. . . . . . . . . 10
Poly Poly deg degAA
coeffdegAA deg degAA coeffdegAA deg |
133 | | simprl3 1108 |
. . . . . . . . . . 11
Poly Poly deg degAA
coeffdegAA deg degAA coeffdegAA coeffdegAA |
134 | 129 | fveq2d 6195 |
. . . . . . . . . . 11
Poly Poly deg degAA
coeffdegAA deg degAA coeffdegAA coeffdeg coeffdegAA |
135 | 129 | fveq2d 6195 |
. . . . . . . . . . . 12
Poly Poly deg degAA
coeffdegAA deg degAA coeffdegAA coeffdeg coeffdegAA |
136 | | simprr3 1111 |
. . . . . . . . . . . 12
Poly Poly deg degAA
coeffdegAA deg degAA coeffdegAA coeffdegAA |
137 | 135, 136 | eqtrd 2656 |
. . . . . . . . . . 11
Poly Poly deg degAA
coeffdegAA deg degAA coeffdegAA coeffdeg |
138 | 133, 134,
137 | 3eqtr4d 2666 |
. . . . . . . . . 10
Poly Poly deg degAA
coeffdegAA deg degAA coeffdegAA coeffdeg coeffdeg |
139 | | eqid 2622 |
. . . . . . . . . . 11
deg deg |
140 | 139 | dgrsub2 37705 |
. . . . . . . . . 10
Poly Poly
deg deg deg coeffdeg coeffdeg deg deg |
141 | 126, 127,
130, 132, 138, 140 | syl23anc 1333 |
. . . . . . . . 9
Poly Poly deg degAA
coeffdegAA deg degAA coeffdegAA deg
deg |
142 | 141, 129 | breqtrd 4679 |
. . . . . . . 8
Poly Poly deg degAA
coeffdegAA deg degAA coeffdegAA deg
degAA |
143 | | dgraa0p 37719 |
. . . . . . . 8
Poly deg
degAA
|
144 | 114, 125,
142, 143 | syl3anc 1326 |
. . . . . . 7
Poly Poly deg degAA
coeffdegAA deg degAA coeffdegAA
|
145 | 113, 144 | mpbid 222 |
. . . . . 6
Poly Poly deg degAA
coeffdegAA deg degAA coeffdegAA |
146 | | df-0p 23437 |
. . . . . 6
|
147 | 145, 146 | syl6eq 2672 |
. . . . 5
Poly Poly deg degAA
coeffdegAA deg degAA coeffdegAA |
148 | | ofsubeq0 11017 |
. . . . . . . 8
|
149 | 49, 148 | mp3an1 1411 |
. . . . . . 7
|
150 | 97, 46, 149 | syl2an 494 |
. . . . . 6
Poly
Poly
|
151 | 150 | ad2antlr 763 |
. . . . 5
Poly Poly deg degAA
coeffdegAA deg degAA coeffdegAA |
152 | 147, 151 | mpbid 222 |
. . . 4
Poly Poly deg degAA
coeffdegAA deg degAA coeffdegAA
|
153 | 152 | ex 450 |
. . 3
Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA |
154 | 153 | ralrimivva 2971 |
. 2
Poly
Polydeg degAA
coeffdegAA deg degAA coeffdegAA |
155 | | fveq2 6191 |
. . . . 5
deg deg |
156 | 155 | eqeq1d 2624 |
. . . 4
deg degAA
deg degAA |
157 | | fveq1 6190 |
. . . . 5
|
158 | 157 | eqeq1d 2624 |
. . . 4
|
159 | | fveq2 6191 |
. . . . . 6
coeff coeff |
160 | 159 | fveq1d 6193 |
. . . . 5
coeffdegAA coeffdegAA |
161 | 160 | eqeq1d 2624 |
. . . 4
coeffdegAA coeffdegAA |
162 | 156, 158,
161 | 3anbi123d 1399 |
. . 3
deg degAA
coeffdegAA
deg degAA coeffdegAA |
163 | 162 | reu4 3400 |
. 2
Polydeg degAA coeffdegAA
Polydeg degAA coeffdegAA Poly Polydeg degAA coeffdegAA deg degAA coeffdegAA |
164 | 93, 154, 163 | sylanbrc 698 |
1
Polydeg degAA coeffdegAA |