Step | Hyp | Ref
| Expression |
1 | | elaa 24071 |
. . . 4
Poly |
2 | 1 | simprbi 480 |
. . 3
Poly |
3 | 2 | adantr 481 |
. 2
Poly |
4 | | aacn 24072 |
. . . . 5
|
5 | | reccl 10692 |
. . . . 5
|
6 | 4, 5 | sylan 488 |
. . . 4
|
7 | 6 | adantr 481 |
. . 3
Poly |
8 | | zsscn 11385 |
. . . . . . 7
|
9 | 8 | a1i 11 |
. . . . . 6
Poly |
10 | | simprl 794 |
. . . . . . . . 9
Poly Poly |
11 | | eldifsn 4317 |
. . . . . . . . 9
Poly
Poly
|
12 | 10, 11 | sylib 208 |
. . . . . . . 8
Poly Poly
|
13 | 12 | simpld 475 |
. . . . . . 7
Poly Poly |
14 | | dgrcl 23989 |
. . . . . . 7
Poly deg |
15 | 13, 14 | syl 17 |
. . . . . 6
Poly deg |
16 | 13 | adantr 481 |
. . . . . . . 8
Poly deg Poly |
17 | | 0z 11388 |
. . . . . . . 8
|
18 | | eqid 2622 |
. . . . . . . . 9
coeff coeff |
19 | 18 | coef2 23987 |
. . . . . . . 8
Poly
coeff |
20 | 16, 17, 19 | sylancl 694 |
. . . . . . 7
Poly deg coeff |
21 | | fznn0sub 12373 |
. . . . . . . 8
deg
deg |
22 | 21 | adantl 482 |
. . . . . . 7
Poly deg deg |
23 | 20, 22 | ffvelrnd 6360 |
. . . . . 6
Poly deg coeffdeg |
24 | 9, 15, 23 | elplyd 23958 |
. . . . 5
Poly degcoeffdeg Poly |
25 | | 0cn 10032 |
. . . . . 6
|
26 | | eqid 2622 |
. . . . . . . . . 10
coeff degcoeffdeg coeff degcoeffdeg |
27 | 26 | coefv0 24004 |
. . . . . . . . 9
degcoeffdeg Poly
degcoeffdeg coeff degcoeffdeg |
28 | 24, 27 | syl 17 |
. . . . . . . 8
Poly degcoeffdeg coeff degcoeffdeg |
29 | 23 | zcnd 11483 |
. . . . . . . . . 10
Poly deg coeffdeg |
30 | | eqidd 2623 |
. . . . . . . . . 10
Poly degcoeffdeg degcoeffdeg |
31 | 24, 15, 29, 30 | coeeq2 23998 |
. . . . . . . . 9
Poly coeff degcoeffdeg
deg coeffdeg |
32 | 31 | fveq1d 6193 |
. . . . . . . 8
Poly coeff degcoeffdeg
deg coeffdeg |
33 | | 0nn0 11307 |
. . . . . . . . . 10
|
34 | | breq1 4656 |
. . . . . . . . . . . 12
deg deg |
35 | | oveq2 6658 |
. . . . . . . . . . . . 13
deg deg |
36 | 35 | fveq2d 6195 |
. . . . . . . . . . . 12
coeffdeg coeffdeg |
37 | 34, 36 | ifbieq1d 4109 |
. . . . . . . . . . 11
deg coeffdeg deg coeffdeg |
38 | | eqid 2622 |
. . . . . . . . . . 11
deg coeffdeg deg coeffdeg |
39 | | fvex 6201 |
. . . . . . . . . . . 12
coeffdeg |
40 | | c0ex 10034 |
. . . . . . . . . . . 12
|
41 | 39, 40 | ifex 4156 |
. . . . . . . . . . 11
deg coeffdeg |
42 | 37, 38, 41 | fvmpt 6282 |
. . . . . . . . . 10
deg coeffdeg deg coeffdeg |
43 | 33, 42 | ax-mp 5 |
. . . . . . . . 9
deg coeffdeg deg coeffdeg |
44 | 15 | nn0ge0d 11354 |
. . . . . . . . . . 11
Poly deg |
45 | 44 | iftrued 4094 |
. . . . . . . . . 10
Poly deg coeffdeg coeffdeg |
46 | 15 | nn0cnd 11353 |
. . . . . . . . . . . 12
Poly deg |
47 | 46 | subid1d 10381 |
. . . . . . . . . . 11
Poly deg deg |
48 | 47 | fveq2d 6195 |
. . . . . . . . . 10
Poly coeffdeg coeffdeg |
49 | 45, 48 | eqtrd 2656 |
. . . . . . . . 9
Poly deg coeffdeg coeffdeg |
50 | 43, 49 | syl5eq 2668 |
. . . . . . . 8
Poly
deg coeffdeg coeffdeg |
51 | 28, 32, 50 | 3eqtrd 2660 |
. . . . . . 7
Poly degcoeffdeg coeffdeg |
52 | 12 | simprd 479 |
. . . . . . . 8
Poly |
53 | | eqid 2622 |
. . . . . . . . . . 11
deg deg |
54 | 53, 18 | dgreq0 24021 |
. . . . . . . . . 10
Poly
coeffdeg |
55 | 13, 54 | syl 17 |
. . . . . . . . 9
Poly
coeffdeg |
56 | 55 | necon3bid 2838 |
. . . . . . . 8
Poly
coeffdeg |
57 | 52, 56 | mpbid 222 |
. . . . . . 7
Poly coeffdeg |
58 | 51, 57 | eqnetrd 2861 |
. . . . . 6
Poly degcoeffdeg |
59 | | ne0p 23963 |
. . . . . 6
degcoeffdeg degcoeffdeg |
60 | 25, 58, 59 | sylancr 695 |
. . . . 5
Poly degcoeffdeg |
61 | | eldifsn 4317 |
. . . . 5
degcoeffdeg Poly degcoeffdeg Poly degcoeffdeg |
62 | 24, 60, 61 | sylanbrc 698 |
. . . 4
Poly degcoeffdeg Poly |
63 | | oveq1 6657 |
. . . . . . . . 9
|
64 | 63 | oveq2d 6666 |
. . . . . . . 8
coeffdeg coeffdeg |
65 | 64 | sumeq2sdv 14435 |
. . . . . . 7
degcoeffdeg degcoeffdeg |
66 | | eqid 2622 |
. . . . . . 7
degcoeffdeg degcoeffdeg |
67 | | sumex 14418 |
. . . . . . 7
degcoeffdeg |
68 | 65, 66, 67 | fvmpt 6282 |
. . . . . 6
degcoeffdeg degcoeffdeg |
69 | 7, 68 | syl 17 |
. . . . 5
Poly degcoeffdeg degcoeffdeg |
70 | 18 | coef3 23988 |
. . . . . . . . . . 11
Poly coeff |
71 | 13, 70 | syl 17 |
. . . . . . . . . 10
Poly coeff |
72 | | elfznn0 12433 |
. . . . . . . . . 10
deg
|
73 | | ffvelrn 6357 |
. . . . . . . . . 10
coeff coeff |
74 | 71, 72, 73 | syl2an 494 |
. . . . . . . . 9
Poly deg coeff |
75 | 4 | ad2antrr 762 |
. . . . . . . . . 10
Poly |
76 | | expcl 12878 |
. . . . . . . . . 10
|
77 | 75, 72, 76 | syl2an 494 |
. . . . . . . . 9
Poly deg |
78 | 74, 77 | mulcld 10060 |
. . . . . . . 8
Poly deg coeff |
79 | 75, 15 | expcld 13008 |
. . . . . . . . 9
Poly deg |
80 | 79 | adantr 481 |
. . . . . . . 8
Poly deg deg |
81 | | simplr 792 |
. . . . . . . . . 10
Poly |
82 | 15 | nn0zd 11480 |
. . . . . . . . . 10
Poly deg |
83 | 75, 81, 82 | expne0d 13014 |
. . . . . . . . 9
Poly deg |
84 | 83 | adantr 481 |
. . . . . . . 8
Poly deg deg |
85 | 78, 80, 84 | divcld 10801 |
. . . . . . 7
Poly deg coeff deg |
86 | | fveq2 6191 |
. . . . . . . . 9
deg
coeff coeff deg |
87 | | oveq2 6658 |
. . . . . . . . 9
deg
deg |
88 | 86, 87 | oveq12d 6668 |
. . . . . . . 8
deg
coeff coeff deg deg |
89 | 88 | oveq1d 6665 |
. . . . . . 7
deg
coeff deg coeff deg deg deg |
90 | 85, 89 | fsumrev2 14514 |
. . . . . 6
Poly degcoeff deg
degcoeff deg deg deg |
91 | 46 | adantr 481 |
. . . . . . . . . . . . 13
Poly deg deg |
92 | 91 | addid2d 10237 |
. . . . . . . . . . . 12
Poly deg deg deg |
93 | 92 | oveq1d 6665 |
. . . . . . . . . . 11
Poly deg deg deg |
94 | 93 | fveq2d 6195 |
. . . . . . . . . 10
Poly deg coeff deg coeffdeg |
95 | 93 | oveq2d 6666 |
. . . . . . . . . . 11
Poly deg deg deg |
96 | 75 | adantr 481 |
. . . . . . . . . . . 12
Poly deg |
97 | 81 | adantr 481 |
. . . . . . . . . . . 12
Poly deg |
98 | | elfznn0 12433 |
. . . . . . . . . . . . . 14
deg
|
99 | 98 | adantl 482 |
. . . . . . . . . . . . 13
Poly deg |
100 | 99 | nn0zd 11480 |
. . . . . . . . . . . 12
Poly deg |
101 | 82 | adantr 481 |
. . . . . . . . . . . 12
Poly deg deg |
102 | 96, 97, 100, 101 | expsubd 13019 |
. . . . . . . . . . 11
Poly deg deg deg |
103 | 95, 102 | eqtrd 2656 |
. . . . . . . . . 10
Poly deg deg deg |
104 | 94, 103 | oveq12d 6668 |
. . . . . . . . 9
Poly deg coeff deg deg coeffdeg deg |
105 | 104 | oveq1d 6665 |
. . . . . . . 8
Poly deg coeff deg deg deg coeffdeg deg deg |
106 | 79 | adantr 481 |
. . . . . . . . . 10
Poly deg deg |
107 | | expcl 12878 |
. . . . . . . . . . 11
|
108 | 75, 98, 107 | syl2an 494 |
. . . . . . . . . 10
Poly deg |
109 | 96, 97, 100 | expne0d 13014 |
. . . . . . . . . 10
Poly deg |
110 | 106, 108,
109 | divcld 10801 |
. . . . . . . . 9
Poly deg deg |
111 | 83 | adantr 481 |
. . . . . . . . 9
Poly deg deg |
112 | 29, 110, 106, 111 | divassd 10836 |
. . . . . . . 8
Poly deg coeffdeg deg deg coeffdeg deg deg |
113 | 106, 111 | dividd 10799 |
. . . . . . . . . . 11
Poly deg deg deg |
114 | 113 | oveq1d 6665 |
. . . . . . . . . 10
Poly deg deg deg |
115 | 106, 108,
106, 109, 111 | divdiv32d 10826 |
. . . . . . . . . 10
Poly deg deg deg deg deg |
116 | 96, 97, 100 | exprecd 13016 |
. . . . . . . . . 10
Poly deg |
117 | 114, 115,
116 | 3eqtr4d 2666 |
. . . . . . . . 9
Poly deg deg deg |
118 | 117 | oveq2d 6666 |
. . . . . . . 8
Poly deg coeffdeg deg deg coeffdeg |
119 | 105, 112,
118 | 3eqtrd 2660 |
. . . . . . 7
Poly deg coeff deg deg deg coeffdeg |
120 | 119 | sumeq2dv 14433 |
. . . . . 6
Poly degcoeff deg deg deg degcoeffdeg |
121 | 90, 120 | eqtrd 2656 |
. . . . 5
Poly degcoeff deg
degcoeffdeg |
122 | 18, 53 | coeid2 23995 |
. . . . . . . . 9
Poly
degcoeff |
123 | 13, 75, 122 | syl2anc 693 |
. . . . . . . 8
Poly degcoeff |
124 | | simprr 796 |
. . . . . . . 8
Poly |
125 | 123, 124 | eqtr3d 2658 |
. . . . . . 7
Poly degcoeff |
126 | 125 | oveq1d 6665 |
. . . . . 6
Poly degcoeff deg deg |
127 | | fzfid 12772 |
. . . . . . 7
Poly deg |
128 | 127, 79, 78, 83 | fsumdivc 14518 |
. . . . . 6
Poly degcoeff deg
degcoeff deg |
129 | 79, 83 | div0d 10800 |
. . . . . 6
Poly deg |
130 | 126, 128,
129 | 3eqtr3d 2664 |
. . . . 5
Poly degcoeff deg |
131 | 69, 121, 130 | 3eqtr2d 2662 |
. . . 4
Poly degcoeffdeg |
132 | | fveq1 6190 |
. . . . . 6
degcoeffdeg degcoeffdeg |
133 | 132 | eqeq1d 2624 |
. . . . 5
degcoeffdeg degcoeffdeg |
134 | 133 | rspcev 3309 |
. . . 4
degcoeffdeg Poly degcoeffdeg Poly |
135 | 62, 131, 134 | syl2anc 693 |
. . 3
Poly Poly |
136 | | elaa 24071 |
. . 3
Poly |
137 | 7, 135, 136 | sylanbrc 698 |
. 2
Poly |
138 | 3, 137 | rexlimddv 3035 |
1
|