Step | Hyp | Ref
| Expression |
1 | | plyco.2 |
. . . . 5
Poly |
2 | | plyf 23954 |
. . . . 5
Poly
|
3 | 1, 2 | syl 17 |
. . . 4
|
4 | 3 | ffvelrnda 6359 |
. . 3
|
5 | 3 | feqmptd 6249 |
. . 3
|
6 | | plyco.1 |
. . . 4
Poly |
7 | | eqid 2622 |
. . . . 5
coeff coeff |
8 | | eqid 2622 |
. . . . 5
deg deg |
9 | 7, 8 | coeid 23994 |
. . . 4
Poly
degcoeff |
10 | 6, 9 | syl 17 |
. . 3
degcoeff |
11 | | oveq1 6657 |
. . . . 5
|
12 | 11 | oveq2d 6666 |
. . . 4
coeff coeff |
13 | 12 | sumeq2sdv 14435 |
. . 3
degcoeff
degcoeff |
14 | 4, 5, 10, 13 | fmptco 6396 |
. 2
degcoeff |
15 | | dgrcl 23989 |
. . . 4
Poly
deg |
16 | 6, 15 | syl 17 |
. . 3
deg |
17 | | oveq2 6658 |
. . . . . . . 8
|
18 | 17 | sumeq1d 14431 |
. . . . . . 7
coeff coeff |
19 | 18 | mpteq2dv 4745 |
. . . . . 6
coeff coeff |
20 | 19 | eleq1d 2686 |
. . . . 5
coeff Poly coeff Poly |
21 | 20 | imbi2d 330 |
. . . 4
coeff Poly
coeff Poly |
22 | | oveq2 6658 |
. . . . . . . 8
|
23 | 22 | sumeq1d 14431 |
. . . . . . 7
coeff coeff |
24 | 23 | mpteq2dv 4745 |
. . . . . 6
coeff coeff |
25 | 24 | eleq1d 2686 |
. . . . 5
coeff Poly coeff Poly |
26 | 25 | imbi2d 330 |
. . . 4
coeff Poly
coeff Poly |
27 | | oveq2 6658 |
. . . . . . . 8
|
28 | 27 | sumeq1d 14431 |
. . . . . . 7
coeff coeff |
29 | 28 | mpteq2dv 4745 |
. . . . . 6
coeff coeff |
30 | 29 | eleq1d 2686 |
. . . . 5
coeff Poly coeff Poly |
31 | 30 | imbi2d 330 |
. . . 4
coeff Poly
coeff Poly |
32 | | oveq2 6658 |
. . . . . . . 8
deg
deg |
33 | 32 | sumeq1d 14431 |
. . . . . . 7
deg
coeff degcoeff |
34 | 33 | mpteq2dv 4745 |
. . . . . 6
deg
coeff degcoeff |
35 | 34 | eleq1d 2686 |
. . . . 5
deg
coeff Poly degcoeff Poly |
36 | 35 | imbi2d 330 |
. . . 4
deg
coeff Poly
degcoeff Poly |
37 | | 0z 11388 |
. . . . . . . . 9
|
38 | 4 | exp0d 13002 |
. . . . . . . . . . . 12
|
39 | 38 | oveq2d 6666 |
. . . . . . . . . . 11
coeff coeff |
40 | | plybss 23950 |
. . . . . . . . . . . . . . . 16
Poly
|
41 | 6, 40 | syl 17 |
. . . . . . . . . . . . . . 15
|
42 | | 0cnd 10033 |
. . . . . . . . . . . . . . . 16
|
43 | 42 | snssd 4340 |
. . . . . . . . . . . . . . 15
|
44 | 41, 43 | unssd 3789 |
. . . . . . . . . . . . . 14
|
45 | 7 | coef 23986 |
. . . . . . . . . . . . . . . 16
Poly
coeff |
46 | 6, 45 | syl 17 |
. . . . . . . . . . . . . . 15
coeff |
47 | | 0nn0 11307 |
. . . . . . . . . . . . . . 15
|
48 | | ffvelrn 6357 |
. . . . . . . . . . . . . . 15
coeff
coeff |
49 | 46, 47, 48 | sylancl 694 |
. . . . . . . . . . . . . 14
coeff |
50 | 44, 49 | sseldd 3604 |
. . . . . . . . . . . . 13
coeff |
51 | 50 | adantr 481 |
. . . . . . . . . . . 12
coeff |
52 | 51 | mulid1d 10057 |
. . . . . . . . . . 11
coeff coeff |
53 | 39, 52 | eqtrd 2656 |
. . . . . . . . . 10
coeff coeff |
54 | 53, 51 | eqeltrd 2701 |
. . . . . . . . 9
coeff |
55 | | fveq2 6191 |
. . . . . . . . . . 11
coeff coeff |
56 | | oveq2 6658 |
. . . . . . . . . . 11
|
57 | 55, 56 | oveq12d 6668 |
. . . . . . . . . 10
coeff coeff |
58 | 57 | fsum1 14476 |
. . . . . . . . 9
coeff coeff coeff |
59 | 37, 54, 58 | sylancr 695 |
. . . . . . . 8
coeff coeff |
60 | 59, 53 | eqtrd 2656 |
. . . . . . 7
coeff coeff |
61 | 60 | mpteq2dva 4744 |
. . . . . 6
coeff coeff |
62 | | fconstmpt 5163 |
. . . . . 6
coeff coeff |
63 | 61, 62 | syl6eqr 2674 |
. . . . 5
coeff coeff |
64 | | plyconst 23962 |
. . . . . . 7
coeff coeff Poly |
65 | 44, 49, 64 | syl2anc 693 |
. . . . . 6
coeff Poly |
66 | | plyun0 23953 |
. . . . . 6
Poly
Poly |
67 | 65, 66 | syl6eleq 2711 |
. . . . 5
coeff Poly |
68 | 63, 67 | eqeltrd 2701 |
. . . 4
coeff Poly |
69 | | simprr 796 |
. . . . . . . . 9
coeff Poly coeff Poly |
70 | 44 | adantr 481 |
. . . . . . . . . . . . 13
|
71 | | peano2nn0 11333 |
. . . . . . . . . . . . . 14
|
72 | | ffvelrn 6357 |
. . . . . . . . . . . . . 14
coeff coeff |
73 | 46, 71, 72 | syl2an 494 |
. . . . . . . . . . . . 13
coeff |
74 | | plyconst 23962 |
. . . . . . . . . . . . 13
coeff coeff Poly |
75 | 70, 73, 74 | syl2anc 693 |
. . . . . . . . . . . 12
coeff Poly |
76 | 75, 66 | syl6eleq 2711 |
. . . . . . . . . . 11
coeff Poly |
77 | | nn0p1nn 11332 |
. . . . . . . . . . . . 13
|
78 | | oveq2 6658 |
. . . . . . . . . . . . . . . . 17
|
79 | 78 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . 16
|
80 | 79 | eleq1d 2686 |
. . . . . . . . . . . . . . 15
Poly
Poly |
81 | 80 | imbi2d 330 |
. . . . . . . . . . . . . 14
Poly
Poly |
82 | | oveq2 6658 |
. . . . . . . . . . . . . . . . 17
|
83 | 82 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . 16
|
84 | 83 | eleq1d 2686 |
. . . . . . . . . . . . . . 15
Poly
Poly |
85 | 84 | imbi2d 330 |
. . . . . . . . . . . . . 14
Poly
Poly |
86 | | oveq2 6658 |
. . . . . . . . . . . . . . . . 17
|
87 | 86 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . 16
|
88 | 87 | eleq1d 2686 |
. . . . . . . . . . . . . . 15
Poly
Poly |
89 | 88 | imbi2d 330 |
. . . . . . . . . . . . . 14
Poly
Poly |
90 | 4 | exp1d 13003 |
. . . . . . . . . . . . . . . . 17
|
91 | 90 | mpteq2dva 4744 |
. . . . . . . . . . . . . . . 16
|
92 | 91, 5 | eqtr4d 2659 |
. . . . . . . . . . . . . . 15
|
93 | 92, 1 | eqeltrd 2701 |
. . . . . . . . . . . . . 14
Poly |
94 | | simprr 796 |
. . . . . . . . . . . . . . . . . . 19
Poly Poly |
95 | 1 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
Poly
Poly |
96 | | plyco.3 |
. . . . . . . . . . . . . . . . . . . 20
|
97 | 96 | adantlr 751 |
. . . . . . . . . . . . . . . . . . 19
Poly |
98 | | plyco.4 |
. . . . . . . . . . . . . . . . . . . 20
|
99 | 98 | adantlr 751 |
. . . . . . . . . . . . . . . . . . 19
Poly |
100 | 94, 95, 97, 99 | plymul 23974 |
. . . . . . . . . . . . . . . . . 18
Poly Poly |
101 | 100 | expr 643 |
. . . . . . . . . . . . . . . . 17
Poly Poly |
102 | | cnex 10017 |
. . . . . . . . . . . . . . . . . . . . 21
|
103 | 102 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
|
104 | | ovexd 6680 |
. . . . . . . . . . . . . . . . . . . 20
|
105 | 4 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . 20
|
106 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . . 20
|
107 | 5 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
108 | 103, 104,
105, 106, 107 | offval2 6914 |
. . . . . . . . . . . . . . . . . . 19
|
109 | | nnnn0 11299 |
. . . . . . . . . . . . . . . . . . . . . 22
|
110 | 109 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . 21
|
111 | 105, 110 | expp1d 13009 |
. . . . . . . . . . . . . . . . . . . 20
|
112 | 111 | mpteq2dva 4744 |
. . . . . . . . . . . . . . . . . . 19
|
113 | 108, 112 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . 18
|
114 | 113 | eleq1d 2686 |
. . . . . . . . . . . . . . . . 17
Poly Poly |
115 | 101, 114 | sylibd 229 |
. . . . . . . . . . . . . . . 16
Poly Poly |
116 | 115 | expcom 451 |
. . . . . . . . . . . . . . 15
Poly
Poly |
117 | 116 | a2d 29 |
. . . . . . . . . . . . . 14
Poly Poly |
118 | 81, 85, 89, 89, 93, 117 | nnind 11038 |
. . . . . . . . . . . . 13
Poly |
119 | 77, 118 | syl 17 |
. . . . . . . . . . . 12
Poly |
120 | 119 | impcom 446 |
. . . . . . . . . . 11
Poly |
121 | 96 | adantlr 751 |
. . . . . . . . . . 11
|
122 | 98 | adantlr 751 |
. . . . . . . . . . 11
|
123 | 76, 120, 121, 122 | plymul 23974 |
. . . . . . . . . 10
coeff Poly |
124 | 123 | adantrr 753 |
. . . . . . . . 9
coeff Poly coeff Poly |
125 | 96 | adantlr 751 |
. . . . . . . . 9
coeff Poly
|
126 | 69, 124, 125 | plyadd 23973 |
. . . . . . . 8
coeff Poly coeff coeff Poly |
127 | 126 | expr 643 |
. . . . . . 7
coeff Poly coeff coeff Poly |
128 | 102 | a1i 11 |
. . . . . . . . . 10
|
129 | | sumex 14418 |
. . . . . . . . . . 11
coeff |
130 | 129 | a1i 11 |
. . . . . . . . . 10
coeff |
131 | | ovexd 6680 |
. . . . . . . . . 10
coeff |
132 | | eqidd 2623 |
. . . . . . . . . 10
coeff coeff |
133 | | fvexd 6203 |
. . . . . . . . . . 11
coeff |
134 | | ovexd 6680 |
. . . . . . . . . . 11
|
135 | | fconstmpt 5163 |
. . . . . . . . . . . 12
coeff coeff |
136 | 135 | a1i 11 |
. . . . . . . . . . 11
coeff coeff |
137 | | eqidd 2623 |
. . . . . . . . . . 11
|
138 | 128, 133,
134, 136, 137 | offval2 6914 |
. . . . . . . . . 10
coeff coeff |
139 | 128, 130,
131, 132, 138 | offval2 6914 |
. . . . . . . . 9
coeff coeff coeff coeff |
140 | | simplr 792 |
. . . . . . . . . . . 12
|
141 | | nn0uz 11722 |
. . . . . . . . . . . 12
|
142 | 140, 141 | syl6eleq 2711 |
. . . . . . . . . . 11
|
143 | 7 | coef3 23988 |
. . . . . . . . . . . . . . 15
Poly
coeff |
144 | 6, 143 | syl 17 |
. . . . . . . . . . . . . 14
coeff |
145 | 144 | ad2antrr 762 |
. . . . . . . . . . . . 13
coeff |
146 | | elfznn0 12433 |
. . . . . . . . . . . . 13
|
147 | | ffvelrn 6357 |
. . . . . . . . . . . . 13
coeff coeff |
148 | 145, 146,
147 | syl2an 494 |
. . . . . . . . . . . 12
coeff |
149 | 4 | adantlr 751 |
. . . . . . . . . . . . 13
|
150 | | expcl 12878 |
. . . . . . . . . . . . 13
|
151 | 149, 146,
150 | syl2an 494 |
. . . . . . . . . . . 12
|
152 | 148, 151 | mulcld 10060 |
. . . . . . . . . . 11
coeff |
153 | | fveq2 6191 |
. . . . . . . . . . . 12
coeff coeff |
154 | | oveq2 6658 |
. . . . . . . . . . . 12
|
155 | 153, 154 | oveq12d 6668 |
. . . . . . . . . . 11
coeff coeff |
156 | 142, 152,
155 | fsump1 14487 |
. . . . . . . . . 10
coeff coeff coeff |
157 | 156 | mpteq2dva 4744 |
. . . . . . . . 9
coeff
coeff coeff |
158 | 139, 157 | eqtr4d 2659 |
. . . . . . . 8
coeff coeff coeff |
159 | 158 | eleq1d 2686 |
. . . . . . 7
coeff coeff Poly coeff Poly |
160 | 127, 159 | sylibd 229 |
. . . . . 6
coeff Poly coeff Poly |
161 | 160 | expcom 451 |
. . . . 5
coeff Poly coeff Poly |
162 | 161 | a2d 29 |
. . . 4
coeff Poly
coeff Poly |
163 | 21, 26, 31, 36, 68, 162 | nn0ind 11472 |
. . 3
deg degcoeff Poly |
164 | 16, 163 | mpcom 38 |
. 2
degcoeff Poly |
165 | 14, 164 | eqeltrd 2701 |
1
Poly |