Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bpolydiflem Structured version   Unicode version

Theorem bpolydiflem 28126
 Description: Lemma for bpolydif 28127. (Contributed by Scott Fenton, 12-Jun-2014.)
Hypotheses
Ref Expression
bpolydiflem.1
bpolydiflem.2
bpolydiflem.3 BernPoly BernPoly
Assertion
Ref Expression
bpolydiflem BernPoly BernPoly
Distinct variable groups:   ,   ,   ,

Proof of Theorem bpolydiflem
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 bpolydiflem.1 . . . . 5
21nnnn0d 10632 . . . 4
3 bpolydiflem.2 . . . . 5
4 peano2cn 9537 . . . . 5
53, 4syl 16 . . . 4
6 bpolyval 28121 . . . 4 BernPoly BernPoly
72, 5, 6syl2anc 656 . . 3 BernPoly BernPoly
8 bpolyval 28121 . . . 4 BernPoly BernPoly
92, 3, 8syl2anc 656 . . 3 BernPoly BernPoly
107, 9oveq12d 6108 . 2 BernPoly BernPoly BernPoly BernPoly
115, 2expcld 12004 . . 3
12 fzfid 11791 . . . 4
13 elfzelz 11449 . . . . . . 7
14 bccl 12094 . . . . . . 7
152, 13, 14syl2an 474 . . . . . 6
1615nn0cnd 10634 . . . . 5
17 elfznn0 11477 . . . . . . 7
18 bpolycl 28124 . . . . . . 7 BernPoly
1917, 5, 18syl2anr 475 . . . . . 6 BernPoly
20 fzssp1 11497 . . . . . . . . . . 11
211nncnd 10334 . . . . . . . . . . . . 13
22 ax-1cn 9336 . . . . . . . . . . . . 13
23 npcan 9615 . . . . . . . . . . . . 13
2421, 22, 23sylancl 657 . . . . . . . . . . . 12
2524oveq2d 6106 . . . . . . . . . . 11
2620, 25syl5sseq 3401 . . . . . . . . . 10
2726sselda 3353 . . . . . . . . 9
28 fznn0sub 11483 . . . . . . . . 9
2927, 28syl 16 . . . . . . . 8
30 nn0p1nn 10615 . . . . . . . 8
3129, 30syl 16 . . . . . . 7
3231nncnd 10334 . . . . . 6
3331nnne0d 10362 . . . . . 6
3419, 32, 33divcld 10103 . . . . 5 BernPoly
3516, 34mulcld 9402 . . . 4 BernPoly
3612, 35fsumcl 13206 . . 3 BernPoly
373, 2expcld 12004 . . 3
38 bpolycl 28124 . . . . . . 7 BernPoly
3917, 3, 38syl2anr 475 . . . . . 6 BernPoly
4039, 32, 33divcld 10103 . . . . 5 BernPoly
4116, 40mulcld 9402 . . . 4 BernPoly
4212, 41fsumcl 13206 . . 3 BernPoly
4311, 36, 37, 42sub4d 9764 . 2 BernPoly BernPoly BernPoly BernPoly
44 addcom 9551 . . . . . . . . . . 11
453, 22, 44sylancl 657 . . . . . . . . . 10
4645oveq1d 6105 . . . . . . . . 9
47 binom1p 13290 . . . . . . . . . 10
483, 2, 47syl2anc 656 . . . . . . . . 9
4946, 48eqtrd 2473 . . . . . . . 8
50 nn0uz 10891 . . . . . . . . . 10
512, 50syl6eleq 2531 . . . . . . . . 9
52 bccl2 12095 . . . . . . . . . . . 12
5352adantl 463 . . . . . . . . . . 11
5453nncnd 10334 . . . . . . . . . 10
55 elfznn0 11477 . . . . . . . . . . 11
56 expcl 11879 . . . . . . . . . . 11
573, 55, 56syl2an 474 . . . . . . . . . 10
5854, 57mulcld 9402 . . . . . . . . 9
59 oveq2 6098 . . . . . . . . . 10
60 oveq2 6098 . . . . . . . . . 10
6159, 60oveq12d 6108 . . . . . . . . 9
6251, 58, 61fsumm1 13216 . . . . . . . 8
63 bcnn 12084 . . . . . . . . . . . 12
642, 63syl 16 . . . . . . . . . . 11
6564oveq1d 6105 . . . . . . . . . 10
6637mulid2d 9400 . . . . . . . . . 10
6765, 66eqtrd 2473 . . . . . . . . 9
6867oveq2d 6106 . . . . . . . 8
6949, 62, 683eqtrd 2477 . . . . . . 7
7069oveq1d 6105 . . . . . 6
7126sselda 3353 . . . . . . . . 9
7271, 58syldan 467 . . . . . . . 8
7312, 72fsumcl 13206 . . . . . . 7
7473, 37pncand 9716 . . . . . 6
7570, 74eqtrd 2473 . . . . 5
76 nnm1nn0 10617 . . . . . . . 8
771, 76syl 16 . . . . . . 7
7877, 50syl6eleq 2531 . . . . . 6
79 oveq2 6098 . . . . . . 7
80 oveq2 6098 . . . . . . 7
8179, 80oveq12d 6108 . . . . . 6
8278, 72, 81fsumm1 13216 . . . . 5
8322a1i 11 . . . . . . . . . 10
8421, 83, 83subsub4d 9746 . . . . . . . . 9
85 df-2 10376 . . . . . . . . . 10
8685oveq2i 6101 . . . . . . . . 9
8784, 86syl6eqr 2491 . . . . . . . 8
8887oveq2d 6106 . . . . . . 7
8988sumeq1d 13174 . . . . . 6
90 bcnm1 27317 . . . . . . . 8
912, 90syl 16 . . . . . . 7
9291oveq1d 6105 . . . . . 6
9389, 92oveq12d 6108 . . . . 5
9475, 82, 933eqtrd 2477 . . . 4
95 oveq2 6098 . . . . . . . . 9
96 oveq1 6097 . . . . . . . . . 10 BernPoly BernPoly
97 oveq2 6098 . . . . . . . . . . 11
9897oveq1d 6105 . . . . . . . . . 10
9996, 98oveq12d 6108 . . . . . . . . 9 BernPoly BernPoly
10095, 99oveq12d 6108 . . . . . . . 8 BernPoly BernPoly
10178, 35, 100fsum1p 13218 . . . . . . 7 BernPoly BernPoly BernPoly
102 bpoly0 28122 . . . . . . . . . . 11 BernPoly
1035, 102syl 16 . . . . . . . . . 10 BernPoly
104103oveq1d 6105 . . . . . . . . 9 BernPoly
105104oveq2d 6106 . . . . . . . 8 BernPoly
106105oveq1d 6105 . . . . . . 7 BernPoly BernPoly BernPoly
107101, 106eqtrd 2473 . . . . . 6 BernPoly BernPoly
108 oveq1 6097 . . . . . . . . . 10 BernPoly BernPoly
109108, 98oveq12d 6108 . . . . . . . . 9 BernPoly BernPoly
11095, 109oveq12d 6108 . . . . . . . 8 BernPoly BernPoly
11178, 41, 110fsum1p 13218 . . . . . . 7 BernPoly BernPoly BernPoly
112 bpoly0 28122 . . . . . . . . . . 11 BernPoly
1133, 112syl 16 . . . . . . . . . 10 BernPoly
114113oveq1d 6105 . . . . . . . . 9 BernPoly
115114oveq2d 6106 . . . . . . . 8 BernPoly
116115oveq1d 6105 . . . . . . 7 BernPoly BernPoly BernPoly
117111, 116eqtrd 2473 . . . . . 6 BernPoly BernPoly
118107, 117oveq12d 6108 . . . . 5 BernPoly BernPoly BernPoly BernPoly
119 0z 10653 . . . . . . . . 9
120 bccl 12094 . . . . . . . . 9
1212, 119, 120sylancl 657 . . . . . . . 8
122121nn0cnd 10634 . . . . . . 7
12321subid1d 9704 . . . . . . . . . . 11
124123, 1eqeltrd 2515 . . . . . . . . . 10
125124peano2nnd 10335 . . . . . . . . 9
126125nnrecred 10363 . . . . . . . 8
127126recnd 9408 . . . . . . 7
128122, 127mulcld 9402 . . . . . 6
129 fzfid 11791 . . . . . . 7
130 fzp1ss 11502 . . . . . . . . . 10
131119, 130ax-mp 5 . . . . . . . . 9
132131sseli 3349 . . . . . . . 8
133132, 35sylan2 471 . . . . . . 7 BernPoly
134129, 133fsumcl 13206 . . . . . 6 BernPoly
135132, 41sylan2 471 . . . . . . 7 BernPoly
136129, 135fsumcl 13206 . . . . . 6 BernPoly
137128, 134, 136pnpcand 9752 . . . . 5 BernPoly BernPoly BernPoly BernPoly
138 1z 10672 . . . . . . . . 9
139138a1i 11 . . . . . . . 8
140 0zd 10654 . . . . . . . 8
1411nnzd 10742 . . . . . . . . 9
142 2z 10674 . . . . . . . . 9
143 zsubcl 10683 . . . . . . . . 9
144141, 142, 143sylancl 657 . . . . . . . 8
145 fzssp1 11497 . . . . . . . . . . 11
146 2m1e1 10432 . . . . . . . . . . . . . 14
147146oveq2i 6101 . . . . . . . . . . . . 13
148 2cnd 10390 . . . . . . . . . . . . . 14
14921, 148, 83subsubd 9743 . . . . . . . . . . . . 13
150147, 149syl5reqr 2488 . . . . . . . . . . . 12
151150oveq2d 6106 . . . . . . . . . . 11
152145, 151syl5sseq 3401 . . . . . . . . . 10
153152sselda 3353 . . . . . . . . 9
154153, 72syldan 467 . . . . . . . 8
155 oveq2 6098 . . . . . . . . 9
156 oveq2 6098 . . . . . . . . 9
157155, 156oveq12d 6108 . . . . . . . 8
158139, 140, 144, 154, 157fsumshft 13243 . . . . . . 7
159150oveq2d 6106 . . . . . . . 8
160159sumeq1d 13174 . . . . . . 7
161158, 160eqtrd 2473 . . . . . 6
162 0p1e1 10429 . . . . . . . . . 10
163162oveq1i 6100 . . . . . . . . 9
164163eleq2i 2505 . . . . . . . 8
165 fzssp1 11497 . . . . . . . . . . . . . 14
16624oveq2d 6106 . . . . . . . . . . . . . 14
167165, 166syl5sseq 3401 . . . . . . . . . . . . 13
168167sselda 3353 . . . . . . . . . . . 12
169 bcm1k 12087 . . . . . . . . . . . 12
170168, 169syl 16 . . . . . . . . . . 11
1711adantr 462 . . . . . . . . . . . . . . 15
172171nncnd 10334 . . . . . . . . . . . . . 14
173 elfznn 11474 . . . . . . . . . . . . . . . 16
174173adantl 463 . . . . . . . . . . . . . . 15
175174nncnd 10334 . . . . . . . . . . . . . 14
17622a1i 11 . . . . . . . . . . . . . 14
177172, 175, 176subsubd 9743 . . . . . . . . . . . . 13
178177oveq1d 6105 . . . . . . . . . . . 12
179178oveq2d 6106 . . . . . . . . . . 11
180170, 179eqtrd 2473 . . . . . . . . . 10
181 bpolydiflem.3 . . . . . . . . . . . 12 BernPoly BernPoly
182181oveq1d 6105 . . . . . . . . . . 11 BernPoly BernPoly
183164, 132sylbir 213 . . . . . . . . . . . . 13
184183, 19sylan2 471 . . . . . . . . . . . 12 BernPoly
185183, 39sylan2 471 . . . . . . . . . . . 12 BernPoly
186183, 32sylan2 471 . . . . . . . . . . . 12
187183, 33sylan2 471 . . . . . . . . . . . 12
188184, 185, 186, 187divsubdird 10142 . . . . . . . . . . 11 BernPoly BernPoly BernPoly BernPoly
1893adantr 462 . . . . . . . . . . . . 13
190 nnm1nn0 10617 . . . . . . . . . . . . . 14
191174, 190syl 16 . . . . . . . . . . . . 13
192189, 191expcld 12004 . . . . . . . . . . . 12
193175, 192, 186, 187div23d 10140 . . . . . . . . . . 11
194182, 188, 1933eqtr3d 2481 . . . . . . . . . 10 BernPoly BernPoly
195180, 194oveq12d 6108 . . . . . . . . 9 BernPoly BernPoly
196183, 16sylan2 471 . . . . . . . . . 10
197184, 186, 187divcld 10103 . . . . . . . . . 10 BernPoly
198185, 186, 187divcld 10103 . . . . . . . . . 10 BernPoly
199196, 197, 198subdid 9796 . . . . . . . . 9 BernPoly BernPoly BernPoly BernPoly
200171nnnn0d 10632 . . . . . . . . . . . . 13
201191nn0zd 10741 . . . . . . . . . . . . 13
202 bccl 12094 . . . . . . . . . . . . 13
203200, 201, 202syl2anc 656 . . . . . . . . . . . 12
204203nn0cnd 10634 . . . . . . . . . . 11
205174nnne0d 10362 . . . . . . . . . . . 12
206186, 175, 205divcld 10103 . . . . . . . . . . 11
207175, 186, 187divcld 10103 . . . . . . . . . . . 12
208207, 192mulcld 9402 . . . . . . . . . . 11
209204, 206, 208mulassd 9405 . . . . . . . . . 10
210186, 175, 187, 205divcan6d 10122 . . . . . . . . . . . . 13
211210oveq1d 6105 . . . . . . . . . . . 12
212206, 207, 192mulassd 9405 . . . . . . . . . . . 12
213192mulid2d 9400 . . . . . . . . . . . 12
214211, 212, 2133eqtr3d 2481 . . . . . . . . . . 11
215214oveq2d 6106 . . . . . . . . . 10
216209, 215eqtrd 2473 . . . . . . . . 9
217195, 199, 2163eqtr3d 2481 . . . . . . . 8 BernPoly BernPoly
218164, 217sylan2b 472 . . . . . . 7 BernPoly BernPoly
219218sumeq2dv 13176 . . . . . 6 BernPoly BernPoly
220129, 133, 135fsumsub 13251 . . . . . 6 BernPoly BernPoly BernPoly BernPoly
221161, 219, 2203eqtr2rd 2480 . . . . 5 BernPoly BernPoly
222118, 137, 2213eqtrd 2477 . . . 4 BernPoly BernPoly
22394, 222oveq12d 6108 . . 3 BernPoly BernPoly
224 fzfid 11791 . . . . 5
225224, 154fsumcl 13206 . . . 4
2263, 77expcld 12004 . . . . 5
22721, 226mulcld 9402 . . . 4
228225, 227pncan2d 9717 . . 3
229223, 228eqtrd 2473 . 2 BernPoly BernPoly
23010, 43, 2293eqtrd 2477 1 BernPoly BernPoly
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 369   wceq 1364   wcel 1761   wne 2604   wss 3325  cfv 5415  (class class class)co 6090  cc 9276  cc0 9278  c1 9279   caddc 9281   cmul 9283   cmin 9591   cdiv 9989  cn 10318  c2 10367  cn0 10575  cz 10642  cuz 10857  cfz 11433  cexp 11861   cbc 12074  csu 13159   BernPoly cbp 28118 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-rep 4400  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371  ax-inf2 7843  ax-cnex 9334  ax-resscn 9335  ax-1cn 9336  ax-icn 9337  ax-addcl 9338  ax-addrcl 9339  ax-mulcl 9340  ax-mulrcl 9341  ax-mulcom 9342  ax-addass 9343  ax-mulass 9344  ax-distr 9345  ax-i2m1 9346  ax-1ne0 9347  ax-1rid 9348  ax-rnegex 9349  ax-rrecex 9350  ax-cnre 9351  ax-pre-lttri 9352  ax-pre-lttrn 9353  ax-pre-ltadd 9354  ax-pre-mulgt0 9355  ax-pre-sup 9356 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-fal 1370  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2261  df-mo 2262  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-nel 2607  df-ral 2718  df-rex 2719  df-reu 2720  df-rmo 2721  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-pss 3341  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-tp 3879  df-op 3881  df-uni 4089  df-int 4126  df-iun 4170  df-br 4290  df-opab 4348  df-mpt 4349  df-tr 4383  df-eprel 4628  df-id 4632  df-po 4637  df-so 4638  df-fr 4675  df-se 4676  df-we 4677  df-ord 4718  df-on 4719  df-lim 4720  df-suc 4721  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-isom 5424  df-riota 6049  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-om 6476  df-1st 6576  df-2nd 6577  df-recs 6828  df-rdg 6862  df-1o 6916  df-oadd 6920  df-er 7097  df-en 7307  df-dom 7308  df-sdom 7309  df-fin 7310  df-sup 7687  df-oi 7720  df-card 8105  df-pnf 9416  df-mnf 9417  df-xr 9418  df-ltxr 9419  df-le 9420  df-sub 9593  df-neg 9594  df-div 9990  df-nn 10319  df-2 10376  df-3 10377  df-n0 10576  df-z 10643  df-uz 10858  df-rp 10988  df-fz 11434  df-fzo 11545  df-seq 11803  df-exp 11862  df-fac 12048  df-bc 12075  df-hash 12100  df-cj 12584  df-re 12585  df-im 12586  df-sqr 12720  df-abs 12721  df-clim 12962  df-sum 13160  df-pred 27554  df-wrecs 27646  df-bpoly 28119 This theorem is referenced by:  bpolydif  28127
 Copyright terms: Public domain W3C validator