MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bcpasc Unicode version

Theorem bcpasc 12399
Description: Pascal's rule for the binomial coefficient, generalized to all integers . Equation 2 of [Gleason] p. 295. (Contributed by NM, 13-Jul-2005.) (Revised by Mario Carneiro, 10-Mar-2014.)
Assertion
Ref Expression
bcpasc

Proof of Theorem bcpasc
StepHypRef Expression
1 peano2nn0 10861 . . . . . 6
2 elfzp12 11786 . . . . . . 7
3 nn0uz 11144 . . . . . . 7
42, 3eleq2s 2565 . . . . . 6
51, 4syl 16 . . . . 5
6 1p0e1 10673 . . . . . . . 8
7 bcn0 12388 . . . . . . . . 9
8 0z 10900 . . . . . . . . . . 11
9 1z 10919 . . . . . . . . . . 11
10 zsubcl 10931 . . . . . . . . . . 11
118, 9, 10mp2an 672 . . . . . . . . . 10
12 0re 9617 . . . . . . . . . . . 12
13 ltm1 10407 . . . . . . . . . . . 12
1412, 13ax-mp 5 . . . . . . . . . . 11
1514orci 390 . . . . . . . . . 10
16 bcval4 12385 . . . . . . . . . 10
1711, 15, 16mp3an23 1316 . . . . . . . . 9
187, 17oveq12d 6314 . . . . . . . 8
19 bcn0 12388 . . . . . . . . 9
201, 19syl 16 . . . . . . . 8
216, 18, 203eqtr4a 2524 . . . . . . 7
22 oveq2 6304 . . . . . . . . 9
23 oveq1 6303 . . . . . . . . . 10
2423oveq2d 6312 . . . . . . . . 9
2522, 24oveq12d 6314 . . . . . . . 8
26 oveq2 6304 . . . . . . . 8
2725, 26eqeq12d 2479 . . . . . . 7
2821, 27syl5ibrcom 222 . . . . . 6
29 simpr 461 . . . . . . . . 9
30 0p1e1 10672 . . . . . . . . . 10
3130oveq1i 6306 . . . . . . . . 9
3229, 31syl6eleq 2555 . . . . . . . 8
33 nn0p1nn 10860 . . . . . . . . . . 11
34 nnuz 11145 . . . . . . . . . . 11
3533, 34syl6eleq 2555 . . . . . . . . . 10
36 fzm1 11787 . . . . . . . . . . 11
3736biimpa 484 . . . . . . . . . 10
3835, 37sylan 471 . . . . . . . . 9
39 nn0cn 10830 . . . . . . . . . . . . . . 15
40 ax-1cn 9571 . . . . . . . . . . . . . . 15
41 pncan 9849 . . . . . . . . . . . . . . 15
4239, 40, 41sylancl 662 . . . . . . . . . . . . . 14
4342oveq2d 6312 . . . . . . . . . . . . 13
4443eleq2d 2527 . . . . . . . . . . . 12
4544biimpa 484 . . . . . . . . . . 11
46 1eluzge0 11153 . . . . . . . . . . . . . . 15
47 fzss1 11751 . . . . . . . . . . . . . . 15
4846, 47ax-mp 5 . . . . . . . . . . . . . 14
4948sseli 3499 . . . . . . . . . . . . 13
50 bcp1n 12394 . . . . . . . . . . . . 13
5149, 50syl 16 . . . . . . . . . . . 12
52 bcrpcl 12386 . . . . . . . . . . . . . . . . 17
5349, 52syl 16 . . . . . . . . . . . . . . . 16
5453rpcnd 11287 . . . . . . . . . . . . . . 15
55 elfzuz2 11720 . . . . . . . . . . . . . . . . . 18
5655, 34syl6eleqr 2556 . . . . . . . . . . . . . . . . 17
5756peano2nnd 10578 . . . . . . . . . . . . . . . 16
5857nncnd 10577 . . . . . . . . . . . . . . 15
5956nncnd 10577 . . . . . . . . . . . . . . . . . 18
60 1cnd 9633 . . . . . . . . . . . . . . . . . 18
61 elfzelz 11717 . . . . . . . . . . . . . . . . . . 19
6261zcnd 10995 . . . . . . . . . . . . . . . . . 18
6359, 60, 62addsubd 9975 . . . . . . . . . . . . . . . . 17
64 fznn0sub 11745 . . . . . . . . . . . . . . . . . 18
65 nn0p1nn 10860 . . . . . . . . . . . . . . . . . 18
6664, 65syl 16 . . . . . . . . . . . . . . . . 17
6763, 66eqeltrd 2545 . . . . . . . . . . . . . . . 16
6867nncnd 10577 . . . . . . . . . . . . . . 15
6967nnne0d 10605 . . . . . . . . . . . . . . 15
7054, 58, 68, 69div12d 10381 . . . . . . . . . . . . . 14
7167nnrpd 11284 . . . . . . . . . . . . . . . . 17
7253, 71rpdivcld 11302 . . . . . . . . . . . . . . . 16
7372rpcnd 11287 . . . . . . . . . . . . . . 15
7458, 73mulcomd 9638 . . . . . . . . . . . . . 14
7570, 74eqtrd 2498 . . . . . . . . . . . . 13
7658, 62npcand 9958 . . . . . . . . . . . . . 14
7776oveq2d 6312 . . . . . . . . . . . . 13
7873, 68, 62adddid 9641 . . . . . . . . . . . . 13
7975, 77, 783eqtr2d 2504 . . . . . . . . . . . 12
8054, 68, 69divcan1d 10346 . . . . . . . . . . . . 13
81 elfznn 11743 . . . . . . . . . . . . . . . 16
8281nnne0d 10605 . . . . . . . . . . . . . . 15
8354, 68, 62, 69, 82divdiv2d 10377 . . . . . . . . . . . . . 14
84 bcm1k 12393 . . . . . . . . . . . . . . . 16
8559, 62, 60subsub3d 9984 . . . . . . . . . . . . . . . . . 18
8685oveq1d 6311 . . . . . . . . . . . . . . . . 17
8786oveq2d 6312 . . . . . . . . . . . . . . . 16
8884, 87eqtrd 2498 . . . . . . . . . . . . . . 15
89 fzelp1 11761 . . . . . . . . . . . . . . . . . . . 20
9057nnzd 10993 . . . . . . . . . . . . . . . . . . . . 21
91 elfzm1b 11785 . . . . . . . . . . . . . . . . . . . . 21
9261, 90, 91syl2anc 661 . . . . . . . . . . . . . . . . . . . 20
9389, 92mpbid 210 . . . . . . . . . . . . . . . . . . 19
9459, 40, 41sylancl 662 . . . . . . . . . . . . . . . . . . . 20
9594oveq2d 6312 . . . . . . . . . . . . . . . . . . 19
9693, 95eleqtrd 2547 . . . . . . . . . . . . . . . . . 18
97 bcrpcl 12386 . . . . . . . . . . . . . . . . . 18
9896, 97syl 16 . . . . . . . . . . . . . . . . 17
9998rpcnd 11287 . . . . . . . . . . . . . . . 16
10081nnrpd 11284 . . . . . . . . . . . . . . . . . 18
10171, 100rpdivcld 11302 . . . . . . . . . . . . . . . . 17
102101rpcnd 11287 . . . . . . . . . . . . . . . 16
103101rpne0d 11290 . . . . . . . . . . . . . . . 16
10454, 99, 102, 103divmul3d 10379 . . . . . . . . . . . . . . 15
10588, 104mpbird 232 . . . . . . . . . . . . . 14
10654, 62, 68, 69div23d 10382 . . . . . . . . . . . . . 14
10783, 105, 1063eqtr3rd 2507 . . . . . . . . . . . . 13
10880, 107oveq12d 6314 . . . . . . . . . . . 12
10951, 79, 1083eqtrrd 2503 . . . . . . . . . . 11
11045, 109syl 16 . . . . . . . . . 10
111 oveq2 6304 . . . . . . . . . . . . 13
11233nnzd 10993 . . . . . . . . . . . . . 14
113 nn0re 10829 . . . . . . . . . . . . . . . 16
114113ltp1d 10501 . . . . . . . . . . . . . . 15
115114olcd 393 . . . . . . . . . . . . . 14
116 bcval4 12385 . . . . . . . . . . . . . 14
117112, 115, 116mpd3an23 1326 . . . . . . . . . . . . 13
118111, 117sylan9eqr 2520 . . . . . . . . . . . 12
119 oveq1 6303 . . . . . . . . . . . . . . 15
120119, 42sylan9eqr 2520 . . . . . . . . . . . . . 14
121120oveq2d 6312 . . . . . . . . . . . . 13
122 bcnn 12390 . . . . . . . . . . . . . 14
123122adantr 465 . . . . . . . . . . . . 13
124121, 123eqtrd 2498 . . . . . . . . . . . 12
125118, 124oveq12d 6314 . . . . . . . . . . 11
126 oveq2 6304 . . . . . . . . . . . 12
127 bcnn 12390 . . . . . . . . . . . . 13
1281, 127syl 16 . . . . . . . . . . . 12
129126, 128sylan9eqr 2520 . . . . . . . . . . 11
13030, 125, 1293eqtr4a 2524 . . . . . . . . . 10
131110, 130jaodan 785 . . . . . . . . 9
13238, 131syldan 470 . . . . . . . 8
13332, 132syldan 470 . . . . . . 7
134133ex 434 . . . . . 6
13528, 134jaod 380 . . . . 5
1365, 135sylbid 215 . . . 4
137136imp 429 . . 3
138137adantlr 714 . 2
139 00id 9776 . . 3
140 fzelp1 11761 . . . . . 6
141140con3i 135 . . . . 5
142 bcval3 12384 . . . . . 6
1431423expa 1196 . . . . 5
144141, 143sylan2 474 . . . 4
145 simpll 753 . . . . 5
146 simplr 755 . . . . . 6
147 peano2zm 10932 . . . . . 6
148146, 147syl 16 . . . . 5
14939adantr 465 . . . . . . . . . 10
150149, 40, 41sylancl 662 . . . . . . . . 9
151150oveq2d 6312 . . . . . . . 8
152151eleq2d 2527 . . . . . . 7
153 id 22 . . . . . . . . 9
1541nn0zd 10992 . . . . . . . . 9
155153, 154, 91syl2anr 478 . . . . . . . 8
156 fzp1ss 11760 . . . . . . . . . . 11
1578, 156ax-mp 5 . . . . . . . . . 10
15831, 157eqsstr3i 3534 . . . . . . . . 9
159158sseli 3499 . . . . . . . 8
160155, 159syl6bir 229 . . . . . . 7
161152, 160sylbird 235 . . . . . 6
162161con3dimp 441 . . . . 5
163 bcval3 12384 . . . . 5
164145, 148, 162, 163syl3anc 1228 . . . 4
165144, 164oveq12d 6314 . . 3
166145, 1syl 16 . . . 4
167 simpr 461 . . . 4
168 bcval3 12384 . . . 4
169166, 146, 167, 168syl3anc 1228 . . 3
170139, 165, 1693eqtr4a 2524 . 2
171138, 170pm2.61dan 791 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184  \/wo 368  /\wa 369  =wceq 1395  e.wcel 1818  C_wss 3475   class class class wbr 4452  `cfv 5593  (class class class)co 6296   cc 9511   cr 9512  0cc0 9513  1c1 9514   caddc 9516   cmul 9518   clt 9649   cmin 9828   cdiv 10231   cn 10561   cn0 10820   cz 10889   cuz 11110   crp 11249   cfz 11701   cbc 12380
This theorem is referenced by:  bccl  12400  bcn2m1  12402  bcn2p1  12403  hashbclem  12501  binomlem  13641  bcxmas  13647  srgbinomlem  17195  bcp1ctr  23554  binomfallfaclem2  29162  dvnmul  31740  bcpascm1  32940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592  ax-cnex 9569  ax-resscn 9570  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-addrcl 9574  ax-mulcl 9575  ax-mulrcl 9576  ax-mulcom 9577  ax-addass 9578  ax-mulass 9579  ax-distr 9580  ax-i2m1 9581  ax-1ne0 9582  ax-1rid 9583  ax-rnegex 9584  ax-rrecex 9585  ax-cnre 9586  ax-pre-lttri 9587  ax-pre-lttrn 9588  ax-pre-ltadd 9589  ax-pre-mulgt0 9590
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-pss 3491  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-tp 4034  df-op 4036  df-uni 4250  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-tr 4546  df-eprel 4796  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-ord 4886  df-on 4887  df-lim 4888  df-suc 4889  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-riota 6257  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6701  df-1st 6800  df-2nd 6801  df-recs 7061  df-rdg 7095  df-er 7330  df-en 7537  df-dom 7538  df-sdom 7539  df-pnf 9651  df-mnf 9652  df-xr 9653  df-ltxr 9654  df-le 9655  df-sub 9830  df-neg 9831  df-div 10232  df-nn 10562  df-n0 10821  df-z 10890  df-uz 11111  df-rp 11250  df-fz 11702  df-seq 12108  df-fac 12354  df-bc 12381
  Copyright terms: Public domain W3C validator