Step | Hyp | Ref
| Expression |
1 | | 4nn0 11311 |
. . 3
|
2 | | bpolyval 14780 |
. . 3
BernPoly BernPoly |
3 | 1, 2 | mpan 706 |
. 2
BernPoly BernPoly |
4 | | 4m1e3 11138 |
. . . . . . 7
|
5 | | df-3 11080 |
. . . . . . 7
|
6 | 4, 5 | eqtri 2644 |
. . . . . 6
|
7 | 6 | oveq2i 6661 |
. . . . 5
|
8 | 7 | sumeq1i 14428 |
. . . 4
BernPoly BernPoly |
9 | | 2eluzge0 11733 |
. . . . . . 7
|
10 | 9 | a1i 11 |
. . . . . 6
|
11 | | elfzelz 12342 |
. . . . . . . . . 10
|
12 | | bccl 13109 |
. . . . . . . . . 10
|
13 | 1, 11, 12 | sylancr 695 |
. . . . . . . . 9
|
14 | 13 | nn0cnd 11353 |
. . . . . . . 8
|
15 | 14 | adantl 482 |
. . . . . . 7
|
16 | | elfznn0 12433 |
. . . . . . . . . 10
|
17 | | bpolycl 14783 |
. . . . . . . . . 10
BernPoly |
18 | 16, 17 | sylan 488 |
. . . . . . . . 9
BernPoly |
19 | 18 | ancoms 469 |
. . . . . . . 8
BernPoly |
20 | | 4re 11097 |
. . . . . . . . . . . . 13
|
21 | 20 | a1i 11 |
. . . . . . . . . . . 12
|
22 | 11 | zred 11482 |
. . . . . . . . . . . 12
|
23 | 21, 22 | resubcld 10458 |
. . . . . . . . . . 11
|
24 | | peano2re 10209 |
. . . . . . . . . . 11
|
25 | 23, 24 | syl 17 |
. . . . . . . . . 10
|
26 | 25 | recnd 10068 |
. . . . . . . . 9
|
27 | 26 | adantl 482 |
. . . . . . . 8
|
28 | | 1red 10055 |
. . . . . . . . . . 11
|
29 | 5 | oveq2i 6661 |
. . . . . . . . . . . . . 14
|
30 | 29 | eleq2i 2693 |
. . . . . . . . . . . . 13
|
31 | | elfzelz 12342 |
. . . . . . . . . . . . . . 15
|
32 | 31 | zred 11482 |
. . . . . . . . . . . . . 14
|
33 | | 3re 11094 |
. . . . . . . . . . . . . . 15
|
34 | 33 | a1i 11 |
. . . . . . . . . . . . . 14
|
35 | 20 | a1i 11 |
. . . . . . . . . . . . . 14
|
36 | | elfzle2 12345 |
. . . . . . . . . . . . . 14
|
37 | | 3lt4 11197 |
. . . . . . . . . . . . . . 15
|
38 | 37 | a1i 11 |
. . . . . . . . . . . . . 14
|
39 | 32, 34, 35, 36, 38 | lelttrd 10195 |
. . . . . . . . . . . . 13
|
40 | 30, 39 | sylbir 225 |
. . . . . . . . . . . 12
|
41 | 22, 21 | posdifd 10614 |
. . . . . . . . . . . 12
|
42 | 40, 41 | mpbid 222 |
. . . . . . . . . . 11
|
43 | | 0lt1 10550 |
. . . . . . . . . . . 12
|
44 | 43 | a1i 11 |
. . . . . . . . . . 11
|
45 | 23, 28, 42, 44 | addgt0d 10602 |
. . . . . . . . . 10
|
46 | 45 | gt0ne0d 10592 |
. . . . . . . . 9
|
47 | 46 | adantl 482 |
. . . . . . . 8
|
48 | 19, 27, 47 | divcld 10801 |
. . . . . . 7
BernPoly |
49 | 15, 48 | mulcld 10060 |
. . . . . 6
BernPoly |
50 | 5 | eqeq2i 2634 |
. . . . . . 7
|
51 | | oveq2 6658 |
. . . . . . . . 9
|
52 | | 4bc3eq4 13115 |
. . . . . . . . 9
|
53 | 51, 52 | syl6eq 2672 |
. . . . . . . 8
|
54 | | oveq1 6657 |
. . . . . . . . 9
BernPoly BernPoly |
55 | | oveq2 6658 |
. . . . . . . . . . 11
|
56 | 55 | oveq1d 6665 |
. . . . . . . . . 10
|
57 | | 4cn 11098 |
. . . . . . . . . . . . 13
|
58 | | 3cn 11095 |
. . . . . . . . . . . . 13
|
59 | | ax-1cn 9994 |
. . . . . . . . . . . . 13
|
60 | | 3p1e4 11153 |
. . . . . . . . . . . . 13
|
61 | 57, 58, 59, 60 | subaddrii 10370 |
. . . . . . . . . . . 12
|
62 | 61 | oveq1i 6660 |
. . . . . . . . . . 11
|
63 | | df-2 11079 |
. . . . . . . . . . 11
|
64 | 62, 63 | eqtr4i 2647 |
. . . . . . . . . 10
|
65 | 56, 64 | syl6eq 2672 |
. . . . . . . . 9
|
66 | 54, 65 | oveq12d 6668 |
. . . . . . . 8
BernPoly
BernPoly |
67 | 53, 66 | oveq12d 6668 |
. . . . . . 7
BernPoly BernPoly |
68 | 50, 67 | sylbir 225 |
. . . . . 6
BernPoly BernPoly |
69 | 10, 49, 68 | fsump1 14487 |
. . . . 5
BernPoly
BernPoly BernPoly |
70 | 63 | oveq2i 6661 |
. . . . . . . 8
|
71 | 70 | sumeq1i 14428 |
. . . . . . 7
BernPoly BernPoly |
72 | | 1eluzge0 11732 |
. . . . . . . . . 10
|
73 | 72 | a1i 11 |
. . . . . . . . 9
|
74 | | fzssp1 12384 |
. . . . . . . . . . . 12
|
75 | 63 | oveq1i 6660 |
. . . . . . . . . . . . 13
|
76 | 75 | oveq2i 6661 |
. . . . . . . . . . . 12
|
77 | 74, 76 | sseqtr4i 3638 |
. . . . . . . . . . 11
|
78 | 77 | sseli 3599 |
. . . . . . . . . 10
|
79 | 78, 49 | sylan2 491 |
. . . . . . . . 9
BernPoly |
80 | 63 | eqeq2i 2634 |
. . . . . . . . . 10
|
81 | | oveq2 6658 |
. . . . . . . . . . . 12
|
82 | | 4bc2eq6 13116 |
. . . . . . . . . . . 12
|
83 | 81, 82 | syl6eq 2672 |
. . . . . . . . . . 11
|
84 | | oveq1 6657 |
. . . . . . . . . . . 12
BernPoly BernPoly |
85 | | oveq2 6658 |
. . . . . . . . . . . . . 14
|
86 | 85 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
87 | | 2cn 11091 |
. . . . . . . . . . . . . . . 16
|
88 | | 2p2e4 11144 |
. . . . . . . . . . . . . . . 16
|
89 | 57, 87, 87, 88 | subaddrii 10370 |
. . . . . . . . . . . . . . 15
|
90 | 89 | oveq1i 6660 |
. . . . . . . . . . . . . 14
|
91 | 90, 5 | eqtr4i 2647 |
. . . . . . . . . . . . 13
|
92 | 86, 91 | syl6eq 2672 |
. . . . . . . . . . . 12
|
93 | 84, 92 | oveq12d 6668 |
. . . . . . . . . . 11
BernPoly
BernPoly |
94 | 83, 93 | oveq12d 6668 |
. . . . . . . . . 10
BernPoly BernPoly |
95 | 80, 94 | sylbir 225 |
. . . . . . . . 9
BernPoly BernPoly |
96 | 73, 79, 95 | fsump1 14487 |
. . . . . . . 8
BernPoly
BernPoly BernPoly |
97 | | 0p1e1 11132 |
. . . . . . . . . . . 12
|
98 | 97 | oveq2i 6661 |
. . . . . . . . . . 11
|
99 | 98 | sumeq1i 14428 |
. . . . . . . . . 10
BernPoly BernPoly |
100 | | 0nn0 11307 |
. . . . . . . . . . . . . 14
|
101 | | nn0uz 11722 |
. . . . . . . . . . . . . 14
|
102 | 100, 101 | eleqtri 2699 |
. . . . . . . . . . . . 13
|
103 | 102 | a1i 11 |
. . . . . . . . . . . 12
|
104 | | 3nn 11186 |
. . . . . . . . . . . . . . . . 17
|
105 | | nnuz 11723 |
. . . . . . . . . . . . . . . . 17
|
106 | 104, 105 | eleqtri 2699 |
. . . . . . . . . . . . . . . 16
|
107 | | fzss2 12381 |
. . . . . . . . . . . . . . . 16
|
108 | 106, 107 | ax-mp 5 |
. . . . . . . . . . . . . . 15
|
109 | | 2p1e3 11151 |
. . . . . . . . . . . . . . . 16
|
110 | 109 | oveq2i 6661 |
. . . . . . . . . . . . . . 15
|
111 | 108, 98, 110 | 3sstr4i 3644 |
. . . . . . . . . . . . . 14
|
112 | 111 | sseli 3599 |
. . . . . . . . . . . . 13
|
113 | 112, 49 | sylan2 491 |
. . . . . . . . . . . 12
BernPoly |
114 | 97 | eqeq2i 2634 |
. . . . . . . . . . . . 13
|
115 | | oveq2 6658 |
. . . . . . . . . . . . . . 15
|
116 | | bcn1 13100 |
. . . . . . . . . . . . . . . 16
|
117 | 1, 116 | ax-mp 5 |
. . . . . . . . . . . . . . 15
|
118 | 115, 117 | syl6eq 2672 |
. . . . . . . . . . . . . 14
|
119 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
BernPoly BernPoly |
120 | | oveq2 6658 |
. . . . . . . . . . . . . . . . 17
|
121 | 120 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
|
122 | 4 | oveq1i 6660 |
. . . . . . . . . . . . . . . . 17
|
123 | | df-4 11081 |
. . . . . . . . . . . . . . . . 17
|
124 | 122, 123 | eqtr4i 2647 |
. . . . . . . . . . . . . . . 16
|
125 | 121, 124 | syl6eq 2672 |
. . . . . . . . . . . . . . 15
|
126 | 119, 125 | oveq12d 6668 |
. . . . . . . . . . . . . 14
BernPoly
BernPoly |
127 | 118, 126 | oveq12d 6668 |
. . . . . . . . . . . . 13
BernPoly BernPoly |
128 | 114, 127 | sylbi 207 |
. . . . . . . . . . . 12
BernPoly BernPoly |
129 | 103, 113,
128 | fsump1 14487 |
. . . . . . . . . . 11
BernPoly
BernPoly BernPoly |
130 | | 0z 11388 |
. . . . . . . . . . . . . 14
|
131 | 59 | a1i 11 |
. . . . . . . . . . . . . . 15
|
132 | | bpolycl 14783 |
. . . . . . . . . . . . . . . . 17
BernPoly |
133 | 100, 132 | mpan 706 |
. . . . . . . . . . . . . . . 16
BernPoly |
134 | | 5cn 11100 |
. . . . . . . . . . . . . . . . 17
|
135 | 134 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
136 | | 0re 10040 |
. . . . . . . . . . . . . . . . . 18
|
137 | | 5pos 11118 |
. . . . . . . . . . . . . . . . . 18
|
138 | 136, 137 | gtneii 10149 |
. . . . . . . . . . . . . . . . 17
|
139 | 138 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
140 | 133, 135,
139 | divcld 10801 |
. . . . . . . . . . . . . . 15
BernPoly
|
141 | 131, 140 | mulcld 10060 |
. . . . . . . . . . . . . 14
BernPoly |
142 | | oveq2 6658 |
. . . . . . . . . . . . . . . . 17
|
143 | | bcn0 13097 |
. . . . . . . . . . . . . . . . . 18
|
144 | 1, 143 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
|
145 | 142, 144 | syl6eq 2672 |
. . . . . . . . . . . . . . . 16
|
146 | | oveq1 6657 |
. . . . . . . . . . . . . . . . 17
BernPoly BernPoly |
147 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . 19
|
148 | 147 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . 18
|
149 | 57 | subid1i 10353 |
. . . . . . . . . . . . . . . . . . . 20
|
150 | 149 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . . 19
|
151 | | 4p1e5 11154 |
. . . . . . . . . . . . . . . . . . 19
|
152 | 150, 151 | eqtri 2644 |
. . . . . . . . . . . . . . . . . 18
|
153 | 148, 152 | syl6eq 2672 |
. . . . . . . . . . . . . . . . 17
|
154 | 146, 153 | oveq12d 6668 |
. . . . . . . . . . . . . . . 16
BernPoly
BernPoly |
155 | 145, 154 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
BernPoly BernPoly |
156 | 155 | fsum1 14476 |
. . . . . . . . . . . . . 14
BernPoly
BernPoly BernPoly |
157 | 130, 141,
156 | sylancr 695 |
. . . . . . . . . . . . 13
BernPoly BernPoly |
158 | | bpoly0 14781 |
. . . . . . . . . . . . . . . 16
BernPoly |
159 | 158 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
BernPoly
|
160 | 159 | oveq2d 6666 |
. . . . . . . . . . . . . 14
BernPoly |
161 | 134, 138 | reccli 10755 |
. . . . . . . . . . . . . . 15
|
162 | 161 | mulid2i 10043 |
. . . . . . . . . . . . . 14
|
163 | 160, 162 | syl6eq 2672 |
. . . . . . . . . . . . 13
BernPoly |
164 | 157, 163 | eqtrd 2656 |
. . . . . . . . . . . 12
BernPoly |
165 | | 1nn0 11308 |
. . . . . . . . . . . . . . 15
|
166 | | bpolycl 14783 |
. . . . . . . . . . . . . . 15
BernPoly |
167 | 165, 166 | mpan 706 |
. . . . . . . . . . . . . 14
BernPoly |
168 | | nn0cn 11302 |
. . . . . . . . . . . . . . 15
|
169 | 1, 168 | mp1i 13 |
. . . . . . . . . . . . . 14
|
170 | | 4ne0 11117 |
. . . . . . . . . . . . . . 15
|
171 | 170 | a1i 11 |
. . . . . . . . . . . . . 14
|
172 | 167, 169,
171 | divcan2d 10803 |
. . . . . . . . . . . . 13
BernPoly BernPoly |
173 | | bpoly1 14782 |
. . . . . . . . . . . . 13
BernPoly |
174 | 172, 173 | eqtrd 2656 |
. . . . . . . . . . . 12
BernPoly |
175 | 164, 174 | oveq12d 6668 |
. . . . . . . . . . 11
BernPoly BernPoly |
176 | 129, 175 | eqtrd 2656 |
. . . . . . . . . 10
BernPoly |
177 | 99, 176 | syl5eqr 2670 |
. . . . . . . . 9
BernPoly |
178 | | 6cn 11102 |
. . . . . . . . . . . 12
|
179 | 178 | a1i 11 |
. . . . . . . . . . 11
|
180 | | 2nn0 11309 |
. . . . . . . . . . . 12
|
181 | | bpolycl 14783 |
. . . . . . . . . . . 12
BernPoly |
182 | 180, 181 | mpan 706 |
. . . . . . . . . . 11
BernPoly |
183 | 58 | a1i 11 |
. . . . . . . . . . 11
|
184 | | 3ne0 11115 |
. . . . . . . . . . . 12
|
185 | 184 | a1i 11 |
. . . . . . . . . . 11
|
186 | 179, 182,
183, 185 | div12d 10837 |
. . . . . . . . . 10
BernPoly BernPoly |
187 | | 3t2e6 11179 |
. . . . . . . . . . . . 13
|
188 | 178, 58, 87, 184 | divmuli 10779 |
. . . . . . . . . . . . 13
|
189 | 187, 188 | mpbir 221 |
. . . . . . . . . . . 12
|
190 | 189 | oveq2i 6661 |
. . . . . . . . . . 11
BernPoly BernPoly |
191 | 87 | a1i 11 |
. . . . . . . . . . . . 13
|
192 | 182, 191 | mulcomd 10061 |
. . . . . . . . . . . 12
BernPoly
BernPoly |
193 | | bpoly2 14788 |
. . . . . . . . . . . . 13
BernPoly |
194 | 193 | oveq2d 6666 |
. . . . . . . . . . . 12
BernPoly |
195 | 192, 194 | eqtrd 2656 |
. . . . . . . . . . 11
BernPoly
|
196 | 190, 195 | syl5eq 2668 |
. . . . . . . . . 10
BernPoly
|
197 | 186, 196 | eqtrd 2656 |
. . . . . . . . 9
BernPoly |
198 | 177, 197 | oveq12d 6668 |
. . . . . . . 8
BernPoly BernPoly |
199 | 96, 198 | eqtrd 2656 |
. . . . . . 7
BernPoly |
200 | 71, 199 | syl5eq 2668 |
. . . . . 6
BernPoly |
201 | | 3nn0 11310 |
. . . . . . . . 9
|
202 | | bpolycl 14783 |
. . . . . . . . 9
BernPoly |
203 | 201, 202 | mpan 706 |
. . . . . . . 8
BernPoly |
204 | | 2ne0 11113 |
. . . . . . . . 9
|
205 | 204 | a1i 11 |
. . . . . . . 8
|
206 | 169, 203,
191, 205 | div12d 10837 |
. . . . . . 7
BernPoly BernPoly |
207 | | 4d2e2 11184 |
. . . . . . . . 9
|
208 | 207 | oveq2i 6661 |
. . . . . . . 8
BernPoly BernPoly |
209 | 203, 191 | mulcomd 10061 |
. . . . . . . . 9
BernPoly
BernPoly |
210 | | bpoly3 14789 |
. . . . . . . . . 10
BernPoly |
211 | 210 | oveq2d 6666 |
. . . . . . . . 9
BernPoly |
212 | 209, 211 | eqtrd 2656 |
. . . . . . . 8
BernPoly
|
213 | 208, 212 | syl5eq 2668 |
. . . . . . 7
BernPoly
|
214 | 206, 213 | eqtrd 2656 |
. . . . . 6
BernPoly |
215 | 200, 214 | oveq12d 6668 |
. . . . 5
BernPoly BernPoly |
216 | 69, 215 | eqtrd 2656 |
. . . 4
BernPoly |
217 | 8, 216 | syl5eq 2668 |
. . 3
BernPoly |
218 | 217 | oveq2d 6666 |
. 2
BernPoly |
219 | | expcl 12878 |
. . . . 5
|
220 | 1, 219 | mpan2 707 |
. . . 4
|
221 | | expcl 12878 |
. . . . . 6
|
222 | 201, 221 | mpan2 707 |
. . . . 5
|
223 | 191, 222 | mulcld 10060 |
. . . 4
|
224 | | sqcl 12925 |
. . . . 5
|
225 | 201, 100 | deccl 11512 |
. . . . . . . 8
; |
226 | 225 | nn0cni 11304 |
. . . . . . 7
; |
227 | | dfdec10 11497 |
. . . . . . . . 9
; ; |
228 | | 10re 11517 |
. . . . . . . . . . . 12
; |
229 | 228 | recni 10052 |
. . . . . . . . . . 11
; |
230 | 229, 58 | mulcli 10045 |
. . . . . . . . . 10
; |
231 | 230 | addid1i 10223 |
. . . . . . . . 9
; ; |
232 | 227, 231 | eqtri 2644 |
. . . . . . . 8
; ; |
233 | | 10pos 11515 |
. . . . . . . . . 10
; |
234 | 136, 233 | gtneii 10149 |
. . . . . . . . 9
; |
235 | 229, 58, 234, 184 | mulne0i 10670 |
. . . . . . . 8
; |
236 | 232, 235 | eqnetri 2864 |
. . . . . . 7
; |
237 | 226, 236 | reccli 10755 |
. . . . . 6
; |
238 | 237 | a1i 11 |
. . . . 5
; |
239 | 224, 238 | subcld 10392 |
. . . 4
; |
240 | 220, 223,
239 | subsubd 10420 |
. . 3
; ; |
241 | 161 | a1i 11 |
. . . . . . . 8
|
242 | | id 22 |
. . . . . . . . 9
|
243 | 87, 204 | reccli 10755 |
. . . . . . . . . 10
|
244 | 243 | a1i 11 |
. . . . . . . . 9
|
245 | 242, 244 | subcld 10392 |
. . . . . . . 8
|
246 | 241, 245 | addcld 10059 |
. . . . . . 7
|
247 | 224, 242 | subcld 10392 |
. . . . . . . . 9
|
248 | | 6pos 11119 |
. . . . . . . . . . . 12
|
249 | 136, 248 | gtneii 10149 |
. . . . . . . . . . 11
|
250 | 178, 249 | reccli 10755 |
. . . . . . . . . 10
|
251 | 250 | a1i 11 |
. . . . . . . . 9
|
252 | 247, 251 | addcld 10059 |
. . . . . . . 8
|
253 | 191, 252 | mulcld 10060 |
. . . . . . 7
|
254 | 246, 253 | addcld 10059 |
. . . . . 6
|
255 | 58, 87, 204 | divcli 10767 |
. . . . . . . . . . 11
|
256 | 255 | a1i 11 |
. . . . . . . . . 10
|
257 | 256, 224 | mulcld 10060 |
. . . . . . . . 9
|
258 | 222, 257 | subcld 10392 |
. . . . . . . 8
|
259 | 244, 242 | mulcld 10060 |
. . . . . . . 8
|
260 | 258, 259 | addcld 10059 |
. . . . . . 7
|
261 | 191, 260 | mulcld 10060 |
. . . . . 6
|
262 | 254, 261 | addcomd 10238 |
. . . . 5
|
263 | 191, 258,
259 | adddid 10064 |
. . . . . . 7
|
264 | 191, 222,
257 | subdid 10486 |
. . . . . . . 8
|
265 | 87, 204 | recidi 10756 |
. . . . . . . . . 10
|
266 | 265 | oveq1i 6660 |
. . . . . . . . 9
|
267 | 191, 244,
242 | mulassd 10063 |
. . . . . . . . 9
|
268 | | mulid2 10038 |
. . . . . . . . 9
|
269 | 266, 267,
268 | 3eqtr3a 2680 |
. . . . . . . 8
|
270 | 264, 269 | oveq12d 6668 |
. . . . . . 7
|
271 | 263, 270 | eqtrd 2656 |
. . . . . 6
|
272 | 271 | oveq1d 6665 |
. . . . 5
|
273 | 191, 257 | mulcld 10060 |
. . . . . . . 8
|
274 | 223, 273 | subcld 10392 |
. . . . . . 7
|
275 | 274, 242,
254 | addassd 10062 |
. . . . . 6
|
276 | 242, 254 | addcld 10059 |
. . . . . . 7
|
277 | 223, 273,
276 | subsubd 10420 |
. . . . . 6
|
278 | 58, 87, 204 | divcan2i 10768 |
. . . . . . . . . . 11
|
279 | 278 | oveq1i 6660 |
. . . . . . . . . 10
|
280 | 191, 256,
224 | mulassd 10063 |
. . . . . . . . . 10
|
281 | 279, 280 | syl5reqr 2671 |
. . . . . . . . 9
|
282 | 281 | oveq1d 6665 |
. . . . . . . 8
|
283 | 242, 246,
253 | add12d 10262 |
. . . . . . . . . 10
|
284 | 191, 247,
251 | adddid 10064 |
. . . . . . . . . . . . . 14
|
285 | 191, 224,
242 | subdid 10486 |
. . . . . . . . . . . . . . 15
|
286 | 187 | oveq2i 6661 |
. . . . . . . . . . . . . . . . 17
|
287 | 58, 184 | reccli 10755 |
. . . . . . . . . . . . . . . . . . . 20
|
288 | 58, 87, 287 | mul32i 10232 |
. . . . . . . . . . . . . . . . . . 19
|
289 | 58, 184 | recidi 10756 |
. . . . . . . . . . . . . . . . . . . . 21
|
290 | 289 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . . . 20
|
291 | 87 | mulid2i 10043 |
. . . . . . . . . . . . . . . . . . . 20
|
292 | 290, 291 | eqtri 2644 |
. . . . . . . . . . . . . . . . . . 19
|
293 | 288, 292 | eqtri 2644 |
. . . . . . . . . . . . . . . . . 18
|
294 | 187, 178 | eqeltri 2697 |
. . . . . . . . . . . . . . . . . . 19
|
295 | 187, 249 | eqnetri 2864 |
. . . . . . . . . . . . . . . . . . 19
|
296 | 87, 294, 287, 295 | divmuli 10779 |
. . . . . . . . . . . . . . . . . 18
|
297 | 293, 296 | mpbir 221 |
. . . . . . . . . . . . . . . . 17
|
298 | 87, 178, 249 | divreci 10770 |
. . . . . . . . . . . . . . . . 17
|
299 | 286, 297,
298 | 3eqtr3ri 2653 |
. . . . . . . . . . . . . . . 16
|
300 | 299 | a1i 11 |
. . . . . . . . . . . . . . 15
|
301 | 285, 300 | oveq12d 6668 |
. . . . . . . . . . . . . 14
|
302 | 284, 301 | eqtrd 2656 |
. . . . . . . . . . . . 13
|
303 | 302 | oveq2d 6666 |
. . . . . . . . . . . 12
|
304 | 191, 224 | mulcld 10060 |
. . . . . . . . . . . . . 14
|
305 | 191, 242 | mulcld 10060 |
. . . . . . . . . . . . . 14
|
306 | 304, 305 | subcld 10392 |
. . . . . . . . . . . . 13
|
307 | 287 | a1i 11 |
. . . . . . . . . . . . 13
|
308 | 242, 306,
307 | addassd 10062 |
. . . . . . . . . . . 12
|
309 | 242, 304,
305 | addsub12d 10415 |
. . . . . . . . . . . . 13
|
310 | 309 | oveq1d 6665 |
. . . . . . . . . . . 12
|
311 | 303, 308,
310 | 3eqtr2d 2662 |
. . . . . . . . . . 11
|
312 | 311 | oveq2d 6666 |
. . . . . . . . . 10
|
313 | 283, 312 | eqtrd 2656 |
. . . . . . . . 9
|
314 | 313 | oveq2d 6666 |
. . . . . . . 8
|
315 | 242, 305 | subcld 10392 |
. . . . . . . . . . . . 13
|
316 | 304, 315 | addcld 10059 |
. . . . . . . . . . . 12
|
317 | 241, 245,
316, 307 | add4d 10264 |
. . . . . . . . . . 11
|
318 | 241, 304,
315 | add12d 10262 |
. . . . . . . . . . . 12
|
319 | 318 | oveq1d 6665 |
. . . . . . . . . . 11
|
320 | 241, 315 | addcld 10059 |
. . . . . . . . . . . 12
|
321 | 245, 307 | addcld 10059 |
. . . . . . . . . . . 12
|
322 | 304, 320,
321 | addassd 10062 |
. . . . . . . . . . 11
|
323 | 317, 319,
322 | 3eqtrd 2660 |
. . . . . . . . . 10
|
324 | 323 | oveq2d 6666 |
. . . . . . . . 9
|
325 | 183, 224 | mulcld 10060 |
. . . . . . . . . 10
|
326 | 320, 321 | addcld 10059 |
. . . . . . . . . 10
|
327 | 325, 304,
326 | subsub4d 10423 |
. . . . . . . . 9
|
328 | 58, 87, 59, 109 | subaddrii 10370 |
. . . . . . . . . . . 12
|
329 | 328 | oveq1i 6660 |
. . . . . . . . . . 11
|
330 | 183, 191,
224 | subdird 10487 |
. . . . . . . . . . 11
|
331 | 224 | mulid2d 10058 |
. . . . . . . . . . 11
|
332 | 329, 330,
331 | 3eqtr3a 2680 |
. . . . . . . . . 10
|
333 | 241, 305,
242 | subsubd 10420 |
. . . . . . . . . . . . 13
|
334 | | 2txmxeqx 11149 |
. . . . . . . . . . . . . 14
|
335 | 334 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
336 | 241, 305,
242 | subadd23d 10414 |
. . . . . . . . . . . . 13
|
337 | 333, 335,
336 | 3eqtr3d 2664 |
. . . . . . . . . . . 12
|
338 | 242, 244,
307 | subsubd 10420 |
. . . . . . . . . . . 12
|
339 | 337, 338 | oveq12d 6668 |
. . . . . . . . . . 11
|
340 | 243, 287 | subcli 10357 |
. . . . . . . . . . . . . 14
|
341 | 340 | a1i 11 |
. . . . . . . . . . . . 13
|
342 | 241, 242,
341 | npncand 10416 |
. . . . . . . . . . . 12
|
343 | | halfthird 11685 |
. . . . . . . . . . . . . 14
|
344 | 343 | oveq2i 6661 |
. . . . . . . . . . . . 13
|
345 | | 5recm6rec 11686 |
. . . . . . . . . . . . 13
; |
346 | 344, 345 | eqtri 2644 |
. . . . . . . . . . . 12
; |
347 | 342, 346 | syl6eq 2672 |
. . . . . . . . . . 11
; |
348 | 339, 347 | eqtr3d 2658 |
. . . . . . . . . 10
; |
349 | 332, 348 | oveq12d 6668 |
. . . . . . . . 9
; |
350 | 324, 327,
349 | 3eqtr2d 2662 |
. . . . . . . 8
; |
351 | 282, 314,
350 | 3eqtrd 2660 |
. . . . . . 7
; |
352 | 351 | oveq2d 6666 |
. . . . . 6
; |
353 | 275, 277,
352 | 3eqtr2d 2662 |
. . . . 5
; |
354 | 262, 272,
353 | 3eqtrd 2660 |
. . . 4
; |
355 | 354 | oveq2d 6666 |
. . 3
; |
356 | 220, 223 | subcld 10392 |
. . . 4
|
357 | 356, 224,
238 | addsubassd 10412 |
. . 3
; ; |
358 | 240, 355,
357 | 3eqtr4d 2666 |
. 2
; |
359 | 3, 218, 358 | 3eqtrd 2660 |
1
BernPoly ; |