Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  bcval5 Unicode version

Theorem bcval5 10537
 Description: Write out the top and bottom parts of the binomial coefficient explicitly. In this form, it is valid even for , although it is no longer valid for nonpositive . (Contributed by Mario Carneiro, 22-May-2014.) (Revised by Jim Kingdon, 23-Apr-2023.)
Assertion
Ref Expression
bcval5

Proof of Theorem bcval5
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 bcval2 10524 . . . 4
3 simprl 521 . . . . . . . . 9
4 simprr 522 . . . . . . . . 9
53, 4mulcld 7806 . . . . . . . 8
6 simpr1 988 . . . . . . . . 9
7 simpr2 989 . . . . . . . . 9
8 simpr3 990 . . . . . . . . 9
96, 7, 8mulassd 7809 . . . . . . . 8
10 simpll 519 . . . . . . . . . . . . 13
1110nn0zd 9191 . . . . . . . . . . . 12
12 simplr 520 . . . . . . . . . . . . 13
1312nnzd 9192 . . . . . . . . . . . 12
1411, 13zsubcld 9198 . . . . . . . . . . 11
1514peano2zd 9196 . . . . . . . . . 10
16 1red 7801 . . . . . . . . . . . 12
1712nnred 8753 . . . . . . . . . . . 12
1810nn0red 9051 . . . . . . . . . . . 12
1912nnge1d 8783 . . . . . . . . . . . 12
2016, 17, 18, 19lesub2dd 8344 . . . . . . . . . . 11
2114zred 9193 . . . . . . . . . . . 12
22 leaddsub 8220 . . . . . . . . . . . 12
2321, 16, 18, 22syl3anc 1217 . . . . . . . . . . 11
2420, 23mpbird 166 . . . . . . . . . 10
25 eluz2 9352 . . . . . . . . . 10
2615, 11, 24, 25syl3anbrc 1166 . . . . . . . . 9
2726adantrr 471 . . . . . . . 8
28 simprr 522 . . . . . . . . 9
29 nnuz 9381 . . . . . . . . 9
3028, 29eleqtrdi 2233 . . . . . . . 8
31 fvi 5482 . . . . . . . . . 10
3231elv 2691 . . . . . . . . 9
33 eluzelcn 9357 . . . . . . . . . 10
3433adantl 275 . . . . . . . . 9
3532, 34eqeltrid 2227 . . . . . . . 8
365, 9, 27, 30, 35seq3split 10279 . . . . . . 7
37 elfzuz3 9830 . . . . . . . . . . 11
3837adantl 275 . . . . . . . . . 10
39 eluznn 9417 . . . . . . . . . 10
4012, 38, 39syl2anc 409 . . . . . . . . 9
4140adantrr 471 . . . . . . . 8
42 facnn 10501 . . . . . . . 8
4341, 42syl 14 . . . . . . 7
44 facnn 10501 . . . . . . . . 9
4528, 44syl 14 . . . . . . . 8
4645oveq1d 5793 . . . . . . 7
4736, 43, 463eqtr4d 2183 . . . . . 6
4847expr 373 . . . . 5
4910faccld 10510 . . . . . . . . 9
5049nncnd 8754 . . . . . . . 8
5150mulid2d 7804 . . . . . . 7
5240, 42syl 14 . . . . . . . 8
5352oveq2d 5794 . . . . . . 7
5451, 53eqtr3d 2175 . . . . . 6
55 fveq2 5425 . . . . . . . . 9
56 fac0 10502 . . . . . . . . 9
5755, 56eqtrdi 2189 . . . . . . . 8
58 oveq1 5785 . . . . . . . . . . 11
59 0p1e1 8854 . . . . . . . . . . 11
6058, 59eqtrdi 2189 . . . . . . . . . 10
6160seqeq1d 10251 . . . . . . . . 9
6261fveq1d 5427 . . . . . . . 8
6357, 62oveq12d 5796 . . . . . . 7
6463eqeq2d 2152 . . . . . 6
6554, 64syl5ibrcom 156 . . . . 5
66 fznn0sub 9864 . . . . . . 7
6766adantl 275 . . . . . 6
68 elnn0 8999 . . . . . 6
6967, 68sylib 121 . . . . 5
7048, 65, 69mpjaod 708 . . . 4
7170oveq1d 5793 . . 3
72 eqid 2140 . . . . . 6
73 fvi 5482 . . . . . . . 8
7473elv 2691 . . . . . . 7
75 eluzelcn 9357 . . . . . . . 8
7675adantl 275 . . . . . . 7
7774, 76eqeltrid 2227 . . . . . 6
78 mulcl 7767 . . . . . . 7
7978adantl 275 . . . . . 6
8072, 15, 77, 79seqf 10261 . . . . 5
8180, 26ffvelrnd 5560 . . . 4
8212nnnn0d 9050 . . . . . 6
8382faccld 10510 . . . . 5
8483nncnd 8754 . . . 4
8567faccld 10510 . . . . 5
8685nncnd 8754 . . . 4
8783nnap0d 8786 . . . 4 #
8885nnap0d 8786 . . . 4 #
8981, 84, 86, 87, 88divcanap5d 8597 . . 3
902, 71, 893eqtrd 2177 . 2
91 simplr 520 . . . . . . 7
9291nnnn0d 9050 . . . . . 6
9392faccld 10510 . . . . 5
9493nncnd 8754 . . . 4
9593nnap0d 8786 . . . 4 #
9694, 95div0apd 8567 . . 3
97 mulcl 7767 . . . . . 6
9897adantl 275 . . . . 5
99 eluzelcn 9357 . . . . . . 7
10099adantl 275 . . . . . 6
10132, 100eqeltrid 2227 . . . . 5
102 simpr 109 . . . . . 6
103102mul02d 8174 . . . . 5
104102mul01d 8175 . . . . 5
105 simpr 109 . . . . . . . . 9
106 nn0uz 9380 . . . . . . . . . . . 12
10792, 106eleqtrdi 2233 . . . . . . . . . . 11
108 simpll 519 . . . . . . . . . . . 12
109108nn0zd 9191 . . . . . . . . . . 11
110 elfz5 9825 . . . . . . . . . . 11
111107, 109, 110syl2anc 409 . . . . . . . . . 10
112 nn0re 9006 . . . . . . . . . . . 12
113112ad2antrr 480 . . . . . . . . . . 11
114 nnre 8747 . . . . . . . . . . . 12
115114ad2antlr 481 . . . . . . . . . . 11
116113, 115subge0d 8317 . . . . . . . . . 10
117111, 116bitr4d 190 . . . . . . . . 9
118105, 117mtbid 662 . . . . . . . 8
119 simpl 108 . . . . . . . . . . . 12
120119nn0zd 9191 . . . . . . . . . . 11
121 simpr 109 . . . . . . . . . . . 12
122121nnzd 9192 . . . . . . . . . . 11
123120, 122zsubcld 9198 . . . . . . . . . 10
124123adantr 274 . . . . . . . . 9
125 0z 9085 . . . . . . . . 9
126 zltnle 9120 . . . . . . . . 9
127124, 125, 126sylancl 410 . . . . . . . 8
128118, 127mpbird 166 . . . . . . 7
129 zltp1le 9128 . . . . . . . 8
130124, 125, 129sylancl 410 . . . . . . 7
131128, 130mpbid 146 . . . . . 6
132 nn0ge0 9022 . . . . . . 7
133132ad2antrr 480 . . . . . 6
134 0zd 9086 . . . . . . 7
135124peano2zd 9196 . . . . . . 7
136 elfz 9823 . . . . . . 7
137134, 135, 109, 136syl3anc 1217 . . . . . 6
138131, 133, 137mpbir2and 929 . . . . 5
139 0cn 7778 . . . . . 6
140 fvi 5482 . . . . . 6
141139, 140mp1i 10 . . . . 5
14298, 101, 103, 104, 138, 141seq3z 10311 . . . 4
143142oveq1d 5793 . . 3
144 nnz 9093 . . . . 5
145 bcval3 10525 . . . . 5
146144, 145syl3an2 1251 . . . 4
1471463expa 1182 . . 3
14896, 143, 1473eqtr4rd 2184 . 2
149 0zd 9086 . . . 4
150 fzdcel 9847 . . . 4 DECID
151122, 149, 120, 150syl3anc 1217 . . 3 DECID
152 exmiddc 822 . . 3 DECID
153151, 152syl 14 . 2
15490, 148, 153mpjaodan 788 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wa 103   wb 104   wo 698  DECID wdc 820   w3a 963   wceq 1332   wcel 1481  cvv 2687   class class class wbr 3933   cid 4214  cfv 5127  (class class class)co 5778  cc 7638  cr 7639  cc0 7640  c1 7641   caddc 7643   cmul 7645   clt 7820   cle 7821   cmin 7953   cdiv 8452  cn 8740  cn0 8997  cz 9074  cuz 9346  cfz 9817   cseq 10245  cfa 10499   cbc 10521 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4047  ax-sep 4050  ax-nul 4058  ax-pow 4102  ax-pr 4135  ax-un 4359  ax-setind 4456  ax-iinf 4506  ax-cnex 7731  ax-resscn 7732  ax-1cn 7733  ax-1re 7734  ax-icn 7735  ax-addcl 7736  ax-addrcl 7737  ax-mulcl 7738  ax-mulrcl 7739  ax-addcom 7740  ax-mulcom 7741  ax-addass 7742  ax-mulass 7743  ax-distr 7744  ax-i2m1 7745  ax-0lt1 7746  ax-1rid 7747  ax-0id 7748  ax-rnegex 7749  ax-precex 7750  ax-cnre 7751  ax-pre-ltirr 7752  ax-pre-ltwlin 7753  ax-pre-lttrn 7754  ax-pre-apti 7755  ax-pre-ltadd 7756  ax-pre-mulgt0 7757  ax-pre-mulext 7758 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-nel 2405  df-ral 2422  df-rex 2423  df-reu 2424  df-rmo 2425  df-rab 2426  df-v 2689  df-sbc 2911  df-csb 3005  df-dif 3074  df-un 3076  df-in 3078  df-ss 3085  df-nul 3365  df-if 3476  df-pw 3513  df-sn 3534  df-pr 3535  df-op 3537  df-uni 3741  df-int 3776  df-iun 3819  df-br 3934  df-opab 3994  df-mpt 3995  df-tr 4031  df-id 4219  df-po 4222  df-iso 4223  df-iord 4292  df-on 4294  df-ilim 4295  df-suc 4297  df-iom 4509  df-xp 4549  df-rel 4550  df-cnv 4551  df-co 4552  df-dm 4553  df-rn 4554  df-res 4555  df-ima 4556  df-iota 5092  df-fun 5129  df-fn 5130  df-f 5131  df-f1 5132  df-fo 5133  df-f1o 5134  df-fv 5135  df-riota 5734  df-ov 5781  df-oprab 5782  df-mpo 5783  df-1st 6042  df-2nd 6043  df-recs 6206  df-frec 6292  df-pnf 7822  df-mnf 7823  df-xr 7824  df-ltxr 7825  df-le 7826  df-sub 7955  df-neg 7956  df-reap 8357  df-ap 8364  df-div 8453  df-inn 8741  df-n0 8998  df-z 9075  df-uz 9347  df-q 9435  df-fz 9818  df-seqfrec 10246  df-fac 10500  df-bc 10522 This theorem is referenced by:  bcn2  10538
 Copyright terms: Public domain W3C validator