Step | Hyp | Ref
| Expression |
1 | | 4nn0 10912 |
. . 3
 |
2 | | bpolyval 14179 |
. . 3
 
  BernPoly                    BernPoly           |
3 | 1, 2 | mpan 684 |
. 2
  BernPoly                    BernPoly           |
4 | | 4cn 10709 |
. . . . . . . 8
 |
5 | | ax-1cn 9615 |
. . . . . . . 8
 |
6 | | 3cn 10706 |
. . . . . . . 8
 |
7 | | 3p1e4 10758 |
. . . . . . . . 9
   |
8 | 6, 5, 7 | addcomli 9843 |
. . . . . . . 8
   |
9 | 4, 5, 6, 8 | subaddrii 9983 |
. . . . . . 7
   |
10 | | df-3 10691 |
. . . . . . 7
   |
11 | 9, 10 | eqtri 2493 |
. . . . . 6
     |
12 | 11 | oveq2i 6319 |
. . . . 5
             |
13 | 12 | sumeq1i 13841 |
. . . 4
             BernPoly                     BernPoly         |
14 | | 2eluzge0 11227 |
. . . . . . 7
     |
15 | 14 | a1i 11 |
. . . . . 6
       |
16 | | elfzelz 11826 |
. . . . . . . . . 10
         |
17 | | bccl 12545 |
. . . . . . . . . 10
 
     |
18 | 1, 16, 17 | sylancr 676 |
. . . . . . . . 9
           |
19 | 18 | nn0cnd 10951 |
. . . . . . . 8
           |
20 | 19 | adantl 473 |
. . . . . . 7
 
           |
21 | | elfznn0 11913 |
. . . . . . . . . 10
         |
22 | | bpolycl 14182 |
. . . . . . . . . 10
 
  BernPoly    |
23 | 21, 22 | sylan 479 |
. . . . . . . . 9
       
  BernPoly    |
24 | 23 | ancoms 460 |
. . . . . . . 8
 
        BernPoly    |
25 | | 4re 10708 |
. . . . . . . . . . . . 13
 |
26 | 25 | a1i 11 |
. . . . . . . . . . . 12
         |
27 | 16 | zred 11063 |
. . . . . . . . . . . 12
         |
28 | 26, 27 | resubcld 10068 |
. . . . . . . . . . 11
           |
29 | | peano2re 9824 |
. . . . . . . . . . 11
         |
30 | 28, 29 | syl 17 |
. . . . . . . . . 10
             |
31 | 30 | recnd 9687 |
. . . . . . . . 9
             |
32 | 31 | adantl 473 |
. . . . . . . 8
 
             |
33 | | 1red 9676 |
. . . . . . . . . . 11
         |
34 | 10 | oveq2i 6319 |
. . . . . . . . . . . . . 14
           |
35 | 34 | eleq2i 2541 |
. . . . . . . . . . . . 13
    
        |
36 | | elfzelz 11826 |
. . . . . . . . . . . . . . 15
       |
37 | 36 | zred 11063 |
. . . . . . . . . . . . . 14
       |
38 | | 3re 10705 |
. . . . . . . . . . . . . . 15
 |
39 | 38 | a1i 11 |
. . . . . . . . . . . . . 14
       |
40 | 25 | a1i 11 |
. . . . . . . . . . . . . 14
       |
41 | | elfzle2 11829 |
. . . . . . . . . . . . . 14
       |
42 | | 3lt4 10802 |
. . . . . . . . . . . . . . 15
 |
43 | 42 | a1i 11 |
. . . . . . . . . . . . . 14
       |
44 | 37, 39, 40, 41, 43 | lelttrd 9810 |
. . . . . . . . . . . . 13
       |
45 | 35, 44 | sylbir 218 |
. . . . . . . . . . . 12
         |
46 | 27, 26 | posdifd 10221 |
. . . . . . . . . . . 12
       
     |
47 | 45, 46 | mpbid 215 |
. . . . . . . . . . 11
           |
48 | | 0lt1 10157 |
. . . . . . . . . . . 12
 |
49 | 48 | a1i 11 |
. . . . . . . . . . 11
         |
50 | 28, 33, 47, 49 | addgt0d 10209 |
. . . . . . . . . 10
             |
51 | 50 | gt0ne0d 10199 |
. . . . . . . . 9
             |
52 | 51 | adantl 473 |
. . . . . . . 8
 
             |
53 | 24, 32, 52 | divcld 10405 |
. . . . . . 7
 
         BernPoly         |
54 | 20, 53 | mulcld 9681 |
. . . . . 6
 
            BernPoly          |
55 | 10 | eqeq2i 2483 |
. . . . . . 7

    |
56 | | oveq2 6316 |
. . . . . . . . 9
       |
57 | | 4bc3eq4 12551 |
. . . . . . . . 9
   |
58 | 56, 57 | syl6eq 2521 |
. . . . . . . 8
     |
59 | | oveq1 6315 |
. . . . . . . . 9
  BernPoly   BernPoly    |
60 | | oveq2 6316 |
. . . . . . . . . . 11
       |
61 | 60 | oveq1d 6323 |
. . . . . . . . . 10
           |
62 | 4, 6, 5, 7 | subaddrii 9983 |
. . . . . . . . . . . 12
   |
63 | 62 | oveq1i 6318 |
. . . . . . . . . . 11
       |
64 | | df-2 10690 |
. . . . . . . . . . 11
   |
65 | 63, 64 | eqtr4i 2496 |
. . . . . . . . . 10
     |
66 | 61, 65 | syl6eq 2521 |
. . . . . . . . 9
       |
67 | 59, 66 | oveq12d 6326 |
. . . . . . . 8
   BernPoly
        BernPoly     |
68 | 58, 67 | oveq12d 6326 |
. . . . . . 7
      BernPoly           BernPoly      |
69 | 55, 68 | sylbir 218 |
. . . . . 6
        BernPoly           BernPoly      |
70 | 15, 54, 69 | fsump1 13894 |
. . . . 5
              BernPoly         
          BernPoly           BernPoly       |
71 | 64 | oveq2i 6319 |
. . . . . . . 8
           |
72 | 71 | sumeq1i 13841 |
. . . . . . 7
           BernPoly                     BernPoly         |
73 | | 1eluzge0 11226 |
. . . . . . . . . 10
     |
74 | 73 | a1i 11 |
. . . . . . . . 9
       |
75 | | fzssp1 11867 |
. . . . . . . . . . . 12
               |
76 | 64 | oveq1i 6318 |
. . . . . . . . . . . . 13
       |
77 | 76 | oveq2i 6319 |
. . . . . . . . . . . 12
               |
78 | 75, 77 | sseqtr4i 3451 |
. . . . . . . . . . 11
             |
79 | 78 | sseli 3414 |
. . . . . . . . . 10
               |
80 | 79, 54 | sylan2 482 |
. . . . . . . . 9
 
            BernPoly          |
81 | 64 | eqeq2i 2483 |
. . . . . . . . . 10

    |
82 | | oveq2 6316 |
. . . . . . . . . . . 12
       |
83 | | 4bc2eq6 12552 |
. . . . . . . . . . . 12
   |
84 | 82, 83 | syl6eq 2521 |
. . . . . . . . . . 11
     |
85 | | oveq1 6315 |
. . . . . . . . . . . 12
  BernPoly   BernPoly    |
86 | | oveq2 6316 |
. . . . . . . . . . . . . 14
       |
87 | 86 | oveq1d 6323 |
. . . . . . . . . . . . 13
           |
88 | | 2cn 10702 |
. . . . . . . . . . . . . . . 16
 |
89 | | 2p2e4 10750 |
. . . . . . . . . . . . . . . 16
   |
90 | 4, 88, 88, 89 | subaddrii 9983 |
. . . . . . . . . . . . . . 15
   |
91 | 90 | oveq1i 6318 |
. . . . . . . . . . . . . 14
       |
92 | 91, 10 | eqtr4i 2496 |
. . . . . . . . . . . . 13
     |
93 | 87, 92 | syl6eq 2521 |
. . . . . . . . . . . 12
       |
94 | 85, 93 | oveq12d 6326 |
. . . . . . . . . . 11
   BernPoly
        BernPoly     |
95 | 84, 94 | oveq12d 6326 |
. . . . . . . . . 10
      BernPoly           BernPoly      |
96 | 81, 95 | sylbir 218 |
. . . . . . . . 9
        BernPoly           BernPoly      |
97 | 74, 80, 96 | fsump1 13894 |
. . . . . . . 8
              BernPoly         
          BernPoly           BernPoly       |
98 | | 0p1e1 10743 |
. . . . . . . . . . . 12
   |
99 | 98 | oveq2i 6319 |
. . . . . . . . . . 11
           |
100 | 99 | sumeq1i 13841 |
. . . . . . . . . 10
             BernPoly                   BernPoly         |
101 | | 0nn0 10908 |
. . . . . . . . . . . . . 14
 |
102 | | nn0uz 11217 |
. . . . . . . . . . . . . 14
     |
103 | 101, 102 | eleqtri 2547 |
. . . . . . . . . . . . 13
     |
104 | 103 | a1i 11 |
. . . . . . . . . . . 12
       |
105 | | 3nn 10791 |
. . . . . . . . . . . . . . . . 17
 |
106 | | nnuz 11218 |
. . . . . . . . . . . . . . . . 17
     |
107 | 105, 106 | eleqtri 2547 |
. . . . . . . . . . . . . . . 16
     |
108 | | fzss2 11864 |
. . . . . . . . . . . . . . . 16
    
          |
109 | 107, 108 | ax-mp 5 |
. . . . . . . . . . . . . . 15
         |
110 | | 2p1e3 10756 |
. . . . . . . . . . . . . . . 16
   |
111 | 110 | oveq2i 6319 |
. . . . . . . . . . . . . . 15
           |
112 | 109, 99, 111 | 3sstr4i 3457 |
. . . . . . . . . . . . . 14
             |
113 | 112 | sseli 3414 |
. . . . . . . . . . . . 13
               |
114 | 113, 54 | sylan2 482 |
. . . . . . . . . . . 12
 
            BernPoly          |
115 | 98 | eqeq2i 2483 |
. . . . . . . . . . . . 13
  
  |
116 | | oveq2 6316 |
. . . . . . . . . . . . . . 15
       |
117 | | bcn1 12536 |
. . . . . . . . . . . . . . . 16

    |
118 | 1, 117 | ax-mp 5 |
. . . . . . . . . . . . . . 15
   |
119 | 116, 118 | syl6eq 2521 |
. . . . . . . . . . . . . 14
     |
120 | | oveq1 6315 |
. . . . . . . . . . . . . . 15
  BernPoly   BernPoly    |
121 | | oveq2 6316 |
. . . . . . . . . . . . . . . . 17
       |
122 | 121 | oveq1d 6323 |
. . . . . . . . . . . . . . . 16
           |
123 | 9 | oveq1i 6318 |
. . . . . . . . . . . . . . . . 17
       |
124 | | df-4 10692 |
. . . . . . . . . . . . . . . . 17
   |
125 | 123, 124 | eqtr4i 2496 |
. . . . . . . . . . . . . . . 16
     |
126 | 122, 125 | syl6eq 2521 |
. . . . . . . . . . . . . . 15
       |
127 | 120, 126 | oveq12d 6326 |
. . . . . . . . . . . . . 14
   BernPoly
        BernPoly     |
128 | 119, 127 | oveq12d 6326 |
. . . . . . . . . . . . 13
      BernPoly           BernPoly      |
129 | 115, 128 | sylbi 200 |
. . . . . . . . . . . 12
        BernPoly           BernPoly      |
130 | 104, 114,
129 | fsump1 13894 |
. . . . . . . . . . 11
              BernPoly         
          BernPoly           BernPoly       |
131 | | 0z 10972 |
. . . . . . . . . . . . . 14
 |
132 | 5 | a1i 11 |
. . . . . . . . . . . . . . 15
   |
133 | | bpolycl 14182 |
. . . . . . . . . . . . . . . . 17
 
  BernPoly    |
134 | 101, 133 | mpan 684 |
. . . . . . . . . . . . . . . 16
  BernPoly    |
135 | | 5cn 10711 |
. . . . . . . . . . . . . . . . 17
 |
136 | 135 | a1i 11 |
. . . . . . . . . . . . . . . 16
   |
137 | | 0re 9661 |
. . . . . . . . . . . . . . . . . 18
 |
138 | | 5pos 10729 |
. . . . . . . . . . . . . . . . . 18
 |
139 | 137, 138 | gtneii 9764 |
. . . . . . . . . . . . . . . . 17
 |
140 | 139 | a1i 11 |
. . . . . . . . . . . . . . . 16
   |
141 | 134, 136,
140 | divcld 10405 |
. . . . . . . . . . . . . . 15
   BernPoly
    |
142 | 132, 141 | mulcld 9681 |
. . . . . . . . . . . . . 14
    BernPoly      |
143 | | oveq2 6316 |
. . . . . . . . . . . . . . . . 17
       |
144 | | bcn0 12533 |
. . . . . . . . . . . . . . . . . 18

    |
145 | 1, 144 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
   |
146 | 143, 145 | syl6eq 2521 |
. . . . . . . . . . . . . . . 16
     |
147 | | oveq1 6315 |
. . . . . . . . . . . . . . . . 17
  BernPoly   BernPoly    |
148 | | oveq2 6316 |
. . . . . . . . . . . . . . . . . . 19
       |
149 | 148 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . 18
           |
150 | 4 | subid1i 9966 |
. . . . . . . . . . . . . . . . . . . 20
   |
151 | 150 | oveq1i 6318 |
. . . . . . . . . . . . . . . . . . 19
       |
152 | | 4p1e5 10759 |
. . . . . . . . . . . . . . . . . . 19
   |
153 | 151, 152 | eqtri 2493 |
. . . . . . . . . . . . . . . . . 18
     |
154 | 149, 153 | syl6eq 2521 |
. . . . . . . . . . . . . . . . 17
       |
155 | 147, 154 | oveq12d 6326 |
. . . . . . . . . . . . . . . 16
   BernPoly
        BernPoly     |
156 | 146, 155 | oveq12d 6326 |
. . . . . . . . . . . . . . 15
      BernPoly           BernPoly      |
157 | 156 | fsum1 13885 |
. . . . . . . . . . . . . 14
     BernPoly
               BernPoly           BernPoly      |
158 | 131, 142,
157 | sylancr 676 |
. . . . . . . . . . . . 13
            BernPoly           BernPoly      |
159 | | bpoly0 14180 |
. . . . . . . . . . . . . . . 16
  BernPoly    |
160 | 159 | oveq1d 6323 |
. . . . . . . . . . . . . . 15
   BernPoly
      |
161 | 160 | oveq2d 6324 |
. . . . . . . . . . . . . 14
    BernPoly          |
162 | 135, 139 | reccli 10359 |
. . . . . . . . . . . . . . 15
   |
163 | 162 | mulid2i 9664 |
. . . . . . . . . . . . . 14
       |
164 | 161, 163 | syl6eq 2521 |
. . . . . . . . . . . . 13
    BernPoly        |
165 | 158, 164 | eqtrd 2505 |
. . . . . . . . . . . 12
            BernPoly            |
166 | | 1nn0 10909 |
. . . . . . . . . . . . . . 15
 |
167 | | bpolycl 14182 |
. . . . . . . . . . . . . . 15
 
  BernPoly    |
168 | 166, 167 | mpan 684 |
. . . . . . . . . . . . . 14
  BernPoly    |
169 | | nn0cn 10903 |
. . . . . . . . . . . . . . 15

  |
170 | 1, 169 | mp1i 13 |
. . . . . . . . . . . . . 14
   |
171 | | 4ne0 10728 |
. . . . . . . . . . . . . . 15
 |
172 | 171 | a1i 11 |
. . . . . . . . . . . . . 14
   |
173 | 168, 170,
172 | divcan2d 10407 |
. . . . . . . . . . . . 13
    BernPoly     BernPoly    |
174 | | bpoly1 14181 |
. . . . . . . . . . . . 13
  BernPoly        |
175 | 173, 174 | eqtrd 2505 |
. . . . . . . . . . . 12
    BernPoly          |
176 | 165, 175 | oveq12d 6326 |
. . . . . . . . . . 11
             BernPoly           BernPoly               |
177 | 130, 176 | eqtrd 2505 |
. . . . . . . . . 10
              BernPoly                  |
178 | 100, 177 | syl5eqr 2519 |
. . . . . . . . 9
            BernPoly                  |
179 | | 6cn 10713 |
. . . . . . . . . . . 12
 |
180 | 179 | a1i 11 |
. . . . . . . . . . 11
   |
181 | | 2nn0 10910 |
. . . . . . . . . . . 12
 |
182 | | bpolycl 14182 |
. . . . . . . . . . . 12
 
  BernPoly    |
183 | 181, 182 | mpan 684 |
. . . . . . . . . . 11
  BernPoly    |
184 | 6 | a1i 11 |
. . . . . . . . . . 11
   |
185 | | 3ne0 10726 |
. . . . . . . . . . . 12
 |
186 | 185 | a1i 11 |
. . . . . . . . . . 11
   |
187 | 180, 183,
184, 186 | div12d 10441 |
. . . . . . . . . 10
    BernPoly      BernPoly       |
188 | | 3t2e6 10784 |
. . . . . . . . . . . . 13
   |
189 | 179, 6, 88, 185 | divmuli 10383 |
. . . . . . . . . . . . 13
  
    |
190 | 188, 189 | mpbir 214 |
. . . . . . . . . . . 12
   |
191 | 190 | oveq2i 6319 |
. . . . . . . . . . 11
  BernPoly       BernPoly    |
192 | 88 | a1i 11 |
. . . . . . . . . . . . 13
   |
193 | 183, 192 | mulcomd 9682 |
. . . . . . . . . . . 12
   BernPoly
    BernPoly     |
194 | | bpoly2 14187 |
. . . . . . . . . . . . 13
  BernPoly              |
195 | 194 | oveq2d 6324 |
. . . . . . . . . . . 12
   BernPoly                 |
196 | 193, 195 | eqtrd 2505 |
. . . . . . . . . . 11
   BernPoly
                |
197 | 191, 196 | syl5eq 2517 |
. . . . . . . . . 10
   BernPoly
                  |
198 | 187, 197 | eqtrd 2505 |
. . . . . . . . 9
    BernPoly                  |
199 | 178, 198 | oveq12d 6326 |
. . . . . . . 8
             BernPoly           BernPoly                             |
200 | 97, 199 | eqtrd 2505 |
. . . . . . 7
              BernPoly                                |
201 | 72, 200 | syl5eq 2517 |
. . . . . 6
            BernPoly                                |
202 | | 3nn0 10911 |
. . . . . . . . 9
 |
203 | | bpolycl 14182 |
. . . . . . . . 9
 
  BernPoly    |
204 | 202, 203 | mpan 684 |
. . . . . . . 8
  BernPoly    |
205 | | 2ne0 10724 |
. . . . . . . . 9
 |
206 | 205 | a1i 11 |
. . . . . . . 8
   |
207 | 170, 204,
192, 206 | div12d 10441 |
. . . . . . 7
    BernPoly      BernPoly       |
208 | | 4d2e2 10789 |
. . . . . . . . 9
   |
209 | 208 | oveq2i 6319 |
. . . . . . . 8
  BernPoly       BernPoly    |
210 | 204, 192 | mulcomd 9682 |
. . . . . . . . 9
   BernPoly
    BernPoly     |
211 | | bpoly3 14188 |
. . . . . . . . . 10
  BernPoly                        |
212 | 211 | oveq2d 6324 |
. . . . . . . . 9
   BernPoly                           |
213 | 210, 212 | eqtrd 2505 |
. . . . . . . 8
   BernPoly
                          |
214 | 209, 213 | syl5eq 2517 |
. . . . . . 7
   BernPoly
                            |
215 | 207, 214 | eqtrd 2505 |
. . . . . 6
    BernPoly                            |
216 | 201, 215 | oveq12d 6326 |
. . . . 5
             BernPoly           BernPoly                                                     |
217 | 70, 216 | eqtrd 2505 |
. . . 4
              BernPoly                                                        |
218 | 13, 217 | syl5eq 2517 |
. . 3
              BernPoly                                                        |
219 | 218 | oveq2d 6324 |
. 2
                   BernPoly                                                               |
220 | | expcl 12328 |
. . . . 5
 
       |
221 | 1, 220 | mpan2 685 |
. . . 4
       |
222 | | expcl 12328 |
. . . . . 6
 
       |
223 | 202, 222 | mpan2 685 |
. . . . 5
       |
224 | 192, 223 | mulcld 9681 |
. . . 4
         |
225 | | sqcl 12375 |
. . . . 5
       |
226 | 202, 101 | deccl 11088 |
. . . . . . . 8
;  |
227 | 226 | nn0cni 10905 |
. . . . . . 7
;  |
228 | | df-dec 11075 |
. . . . . . . . 9
;      |
229 | | 10re 10720 |
. . . . . . . . . . . 12
 |
230 | 229 | recni 9673 |
. . . . . . . . . . 11
 |
231 | 230, 6 | mulcli 9666 |
. . . . . . . . . 10
   |
232 | 231 | addid1i 9838 |
. . . . . . . . 9
       |
233 | 228, 232 | eqtri 2493 |
. . . . . . . 8
;    |
234 | | 10pos 10734 |
. . . . . . . . . 10
 |
235 | 137, 234 | gtneii 9764 |
. . . . . . . . 9
 |
236 | 230, 6, 235, 185 | mulne0i 10277 |
. . . . . . . 8
   |
237 | 233, 236 | eqnetri 2713 |
. . . . . . 7
;  |
238 | 227, 237 | reccli 10359 |
. . . . . 6
 ;   |
239 | 238 | a1i 11 |
. . . . 5
 
;    |
240 | 225, 239 | subcld 10005 |
. . . 4
       ;     |
241 | 221, 224,
240 | subsubd 10033 |
. . 3
                   ;                        ;      |
242 | 162 | a1i 11 |
. . . . . . . 8
     |
243 | | id 22 |
. . . . . . . . 9
   |
244 | 88, 205 | reccli 10359 |
. . . . . . . . . 10
   |
245 | 244 | a1i 11 |
. . . . . . . . 9
     |
246 | 243, 245 | subcld 10005 |
. . . . . . . 8
 
     |
247 | 242, 246 | addcld 9680 |
. . . . . . 7
           |
248 | 225, 243 | subcld 10005 |
. . . . . . . . 9
         |
249 | | 6pos 10730 |
. . . . . . . . . . . 12
 |
250 | 137, 249 | gtneii 9764 |
. . . . . . . . . . 11
 |
251 | 179, 250 | reccli 10359 |
. . . . . . . . . 10
   |
252 | 251 | a1i 11 |
. . . . . . . . 9
     |
253 | 248, 252 | addcld 9680 |
. . . . . . . 8
             |
254 | 192, 253 | mulcld 9681 |
. . . . . . 7
               |
255 | 247, 254 | addcld 9680 |
. . . . . 6
                         |
256 | 6, 88, 205 | divcli 10371 |
. . . . . . . . . . 11
   |
257 | 256 | a1i 11 |
. . . . . . . . . 10
     |
258 | 257, 225 | mulcld 9681 |
. . . . . . . . 9
           |
259 | 223, 258 | subcld 10005 |
. . . . . . . 8
                 |
260 | 245, 243 | mulcld 9681 |
. . . . . . . 8
       |
261 | 259, 260 | addcld 9680 |
. . . . . . 7
                       |
262 | 192, 261 | mulcld 9681 |
. . . . . 6
                         |
263 | 255, 262 | addcomd 9853 |
. . . . 5
                                                                                               |
264 | 192, 259,
260 | adddid 9685 |
. . . . . . 7
                                                 |
265 | 192, 223,
258 | subdid 10095 |
. . . . . . . 8
                                     |
266 | 88, 205 | recidi 10360 |
. . . . . . . . . 10
     |
267 | 266 | oveq1i 6318 |
. . . . . . . . 9
         |
268 | 192, 245,
243 | mulassd 9684 |
. . . . . . . . 9
               |
269 | | mulid2 9659 |
. . . . . . . . 9
     |
270 | 267, 268,
269 | 3eqtr3a 2529 |
. . . . . . . 8
         |
271 | 265, 270 | oveq12d 6326 |
. . . . . . 7
                                               |
272 | 264, 271 | eqtrd 2505 |
. . . . . 6
                                             |
273 | 272 | oveq1d 6323 |
. . . . 5
                                                                                             |
274 | 192, 258 | mulcld 9681 |
. . . . . . . 8
             |
275 | 224, 274 | subcld 10005 |
. . . . . . 7
                     |
276 | 275, 243,
255 | addassd 9683 |
. . . . . 6
                                                                                           |
277 | 243, 255 | addcld 9680 |
. . . . . . 7
 
                         |
278 | 224, 274,
277 | subsubd 10033 |
. . . . . 6
                   
                                                                       |
279 | 6, 88, 205 | divcan2i 10372 |
. . . . . . . . . . 11
     |
280 | 279 | oveq1i 6318 |
. . . . . . . . . 10
                 |
281 | 192, 257,
225 | mulassd 9684 |
. . . . . . . . . 10
                       |
282 | 280, 281 | syl5reqr 2520 |
. . . . . . . . 9
                   |
283 | 282 | oveq1d 6323 |
. . . . . . . 8
                                            
                          |
284 | 243, 247,
254 | add12d 9876 |
. . . . . . . . . 10
 
                                                 |
285 | 192, 248,
252 | adddid 9685 |
. . . . . . . . . . . . . 14
                             |
286 | 192, 225,
243 | subdid 10095 |
. . . . . . . . . . . . . . 15
                     |
287 | 188 | oveq2i 6319 |
. . . . . . . . . . . . . . . . 17
       |
288 | 6, 185 | reccli 10359 |
. . . . . . . . . . . . . . . . . . . 20
   |
289 | 6, 88, 288 | mul32i 9847 |
. . . . . . . . . . . . . . . . . . 19
             |
290 | 6, 185 | recidi 10360 |
. . . . . . . . . . . . . . . . . . . . 21
     |
291 | 290 | oveq1i 6318 |
. . . . . . . . . . . . . . . . . . . 20
         |
292 | 88 | mulid2i 9664 |
. . . . . . . . . . . . . . . . . . . 20
   |
293 | 291, 292 | eqtri 2493 |
. . . . . . . . . . . . . . . . . . 19
       |
294 | 289, 293 | eqtri 2493 |
. . . . . . . . . . . . . . . . . 18
       |
295 | 188, 179 | eqeltri 2545 |
. . . . . . . . . . . . . . . . . . 19
   |
296 | 188, 250 | eqnetri 2713 |
. . . . . . . . . . . . . . . . . . 19
   |
297 | 88, 295, 288, 296 | divmuli 10383 |
. . . . . . . . . . . . . . . . . 18
      
        |
298 | 294, 297 | mpbir 214 |
. . . . . . . . . . . . . . . . 17
       |
299 | 88, 179, 250 | divreci 10374 |
. . . . . . . . . . . . . . . . 17
       |
300 | 287, 298,
299 | 3eqtr3ri 2502 |
. . . . . . . . . . . . . . . 16
       |
301 | 300 | a1i 11 |
. . . . . . . . . . . . . . 15
         |
302 | 286, 301 | oveq12d 6326 |
. . . . . . . . . . . . . 14
                               |
303 | 285, 302 | eqtrd 2505 |
. . . . . . . . . . . . 13
                             |
304 | 303 | oveq2d 6324 |
. . . . . . . . . . . 12
 
                               |
305 | 192, 225 | mulcld 9681 |
. . . . . . . . . . . . . 14
         |
306 | 192, 243 | mulcld 9681 |
. . . . . . . . . . . . . 14
     |
307 | 305, 306 | subcld 10005 |
. . . . . . . . . . . . 13
             |
308 | 288 | a1i 11 |
. . . . . . . . . . . . 13
     |
309 | 243, 307,
308 | addassd 9683 |
. . . . . . . . . . . 12
                                   |
310 | 243, 305,
306 | addsub12d 10028 |
. . . . . . . . . . . . 13
 
                         |
311 | 310 | oveq1d 6323 |
. . . . . . . . . . . 12
                                   |
312 | 304, 309,
311 | 3eqtr2d 2511 |
. . . . . . . . . . 11
 
                               |
313 | 312 | oveq2d 6324 |
. . . . . . . . . 10
                                                     |
314 | 284, 313 | eqtrd 2505 |
. . . . . . . . 9
 
                                                   |
315 | 314 | oveq2d 6324 |
. . . . . . . 8
                                                                     |
316 | 243, 306 | subcld 10005 |
. . . . . . . . . . . . 13
 
     |
317 | 305, 316 | addcld 9680 |
. . . . . . . . . . . 12
               |
318 | 242, 246,
317, 308 | add4d 9878 |
. . . . . . . . . . 11
                                                       |
319 | 242, 305,
316 | add12d 9876 |
. . . . . . . . . . . 12
                                   |
320 | 319 | oveq1d 6323 |
. . . . . . . . . . 11
                                                       |
321 | 242, 316 | addcld 9680 |
. . . . . . . . . . . 12
           |
322 | 246, 308 | addcld 9680 |
. . . . . . . . . . . 12
           |
323 | 305, 321,
322 | addassd 9683 |
. . . . . . . . . . 11
                                                       |
324 | 318, 320,
323 | 3eqtrd 2509 |
. . . . . . . . . 10
                                                       |
325 | 324 | oveq2d 6324 |
. . . . . . . . 9
                                                                       |
326 | 184, 225 | mulcld 9681 |
. . . . . . . . . 10
         |
327 | 321, 322 | addcld 9680 |
. . . . . . . . . 10
                     |
328 | 326, 305,
327 | subsub4d 10036 |
. . . . . . . . 9
                                                                       |
329 | 6, 88, 5, 110 | subaddrii 9983 |
. . . . . . . . . . . 12
   |
330 | 329 | oveq1i 6318 |
. . . . . . . . . . 11
               |
331 | 184, 192,
225 | subdird 10096 |
. . . . . . . . . . 11
                         |
332 | 225 | mulid2d 9679 |
. . . . . . . . . . 11
             |
333 | 330, 331,
332 | 3eqtr3a 2529 |
. . . . . . . . . 10
                     |
334 | 242, 306,
243 | subsubd 10033 |
. . . . . . . . . . . . 13
                   |
335 | 269 | oveq2d 6324 |
. . . . . . . . . . . . . . 15
             |
336 | | 2m1e1 10746 |
. . . . . . . . . . . . . . . . 17
   |
337 | 336 | oveq1i 6318 |
. . . . . . . . . . . . . . . 16
       |
338 | 192, 132,
243 | subdird 10096 |
. . . . . . . . . . . . . . . 16
             |
339 | 337, 338,
269 | 3eqtr3a 2529 |
. . . . . . . . . . . . . . 15
         |
340 | 335, 339 | eqtr3d 2507 |
. . . . . . . . . . . . . 14
       |
341 | 340 | oveq2d 6324 |
. . . . . . . . . . . . 13
               |
342 | 242, 306,
243 | subadd23d 10027 |
. . . . . . . . . . . . 13
                   |
343 | 334, 341,
342 | 3eqtr3d 2513 |
. . . . . . . . . . . 12
               |
344 | 243, 245,
308 | subsubd 10033 |
. . . . . . . . . . . 12
 
                 |
345 | 343, 344 | oveq12d 6326 |
. . . . . . . . . . 11
                                   |
346 | 244, 288 | subcli 9970 |
. . . . . . . . . . . . . 14
       |
347 | 346 | a1i 11 |
. . . . . . . . . . . . 13
         |
348 | 242, 243,
347 | npncand 10029 |
. . . . . . . . . . . 12
                           |
349 | | halfthird 11180 |
. . . . . . . . . . . . . 14
         |
350 | 349 | oveq2i 6319 |
. . . . . . . . . . . . 13
                 |
351 | | 5recm6rec 11181 |
. . . . . . . . . . . . 13
       ;   |
352 | 350, 351 | eqtri 2493 |
. . . . . . . . . . . 12
           ;   |
353 | 348, 352 | syl6eq 2521 |
. . . . . . . . . . 11
                ;    |
354 | 345, 353 | eqtr3d 2507 |
. . . . . . . . . 10
                    ;    |
355 | 333, 354 | oveq12d 6326 |
. . . . . . . . 9
                                         ;     |
356 | 325, 328,
355 | 3eqtr2d 2511 |
. . . . . . . 8
                                        
;     |
357 | 283, 315,
356 | 3eqtrd 2509 |
. . . . . . 7
                                           ;     |
358 | 357 | oveq2d 6324 |
. . . . . 6
                   
                                      ;      |
359 | 276, 278,
358 | 3eqtr2d 2511 |
. . . . 5
                                                         
;      |
360 | 263, 273,
359 | 3eqtrd 2509 |
. . . 4
                                                           
;      |
361 | 360 | oveq2d 6324 |
. . 3
                                                                       ;       |
362 | 221, 224 | subcld 10005 |
. . . 4
               |
363 | 362, 225,
239 | addsubassd 10025 |
. . 3
                     ;                      ;      |
364 | 241, 361,
363 | 3eqtr4d 2515 |
. 2
                                                                        
;     |
365 | 3, 219, 364 | 3eqtrd 2509 |
1
  BernPoly                      ;     |