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

Theorem elfznn0 11075
Description: A member of a finite set of sequential integers starting at 0 is a nonnegative integer. (Contributed by NM, 5-Aug-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
Assertion
Ref Expression
elfznn0  |-  ( K  e.  ( 0 ... N )  ->  K  e.  NN0 )

Proof of Theorem elfznn0
StepHypRef Expression
1 elfz2nn0 11074 . 2  |-  ( K  e.  ( 0 ... N )  <->  ( K  e.  NN0  /\  N  e. 
NN0  /\  K  <_  N ) )
21simp1bi 972 1  |-  ( K  e.  ( 0 ... N )  ->  K  e.  NN0 )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   class class class wbr 4204  (class class class)co 6073   0cc0 8982    <_ cle 9113   NN0cn0 10213   ...cfz 11035
This theorem is referenced by:  bcrpcl  11591  bccmpl  11592  bcp1n  11599  bcp1nk  11600  bcval5  11601  permnn  11609  swrd0len  11761  splfv2a  11777  binomlem  12600  binom1p  12602  binom1dif  12604  bcxmas  12607  climcnds  12623  arisum  12631  arisum2  12632  geolim  12639  geo2sum  12642  mertenslem1  12653  mertenslem2  12654  mertens  12655  efcvgfsum  12680  efcj  12686  efaddlem  12687  effsumlt  12704  eirrlem  12795  fzo0dvdseq  12894  3dvds  12904  prmdiveq  13167  pcbc  13261  vdwapf  13332  vdwlem2  13342  vdwlem6  13346  vdwlem8  13348  efgcpbllemb  15379  psrbaglefi  16429  coe1mul2lem2  16653  coe1mul2  16654  coe1tmmul2  16660  coe1tmmul  16661  mbfi1fseqlem3  19601  mbfi1fseqlem4  19602  itg0  19663  itgz  19664  itgcl  19667  iblabsr  19713  iblmulc2  19714  itgsplit  19719  dvn2bss  19808  coe1mul3  20014  elply2  20107  plyf  20109  elplyd  20113  ply1termlem  20114  plyeq0lem  20121  plypf1  20123  plyaddlem1  20124  plymullem1  20125  plyaddlem  20126  plymullem  20127  coeeulem  20135  coeidlem  20148  coeid3  20151  plyco  20152  coeeq2  20153  dgreq  20155  coefv0  20158  coeaddlem  20159  coemullem  20160  coemulhi  20164  coemulc  20165  coe1termlem  20168  plycn  20171  plycjlem  20186  plycj  20187  plyrecj  20189  dvply1  20193  dvply2g  20194  vieta1lem2  20220  elqaalem2  20229  elqaalem3  20230  aareccl  20235  aannenlem1  20237  aalioulem1  20241  taylply2  20276  taylply  20277  dvtaylp  20278  dvntaylp0  20280  taylthlem2  20282  pserulm  20330  psercn2  20331  pserdvlem2  20336  abelthlem6  20344  abelthlem7  20346  abelthlem8  20347  advlogexp  20538  cxpeq  20633  log2tlbnd  20777  log2ublem2  20779  log2ub  20781  birthdaylem2  20783  birthdaylem3  20784  ftalem1  20847  ftalem5  20851  basellem2  20856  basellem3  20857  dvdsppwf1o  20963  musum  20968  sgmppw  20973  1sgmprm  20975  logexprlim  21001  mersenne  21003  lgseisenlem1  21125  dchrisum0flblem1  21194  pntpbnd2  21273  iseupa  21679  eupares  21689  bcm1n  24143  subfacval2  24865  subfaclim  24866  cvmliftlem7  24970  risefacval2  25318  fallfacval2  25319  fallfacval3  25320  risefaccllem  25321  fallfaccllem  25322  risefacp1  25337  fallfacp1  25338  fallfacfwd  25344  binomfallfaclem1  25347  binomfallfaclem2  25348  binomrisefac  25350  bcfallfac  25352  bpolylem  26086  bpolysum  26091  bpolydiflem  26092  fsumkthpow  26094  bpoly4  26097  iblmulc2nc  26260  jm2.22  27057  jm2.23  27058  hbt  27302  cnsrplycl  27340  psgnunilem2  27386  hashgcdlem  27484  2elfz3nn0  28096  fz0addcom  28097  2elfz2melfz  28101  fz0fzdiffz0  28103  fz0addge0  28104  swrdswrd0  28167  swrd0swrd0  28168  swrdccat3  28181  swrdccat3a  28183  swrdccat3blem  28184  cshwlen  28207  2cshw1lem3  28216  2cshw1  28217  2cshw2lem3  28220  2cshw2  28221  2cshw  28222  cshwssizelem2  28244
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693  ax-cnex 9038  ax-resscn 9039  ax-1cn 9040  ax-icn 9041  ax-addcl 9042  ax-addrcl 9043  ax-mulcl 9044  ax-mulrcl 9045  ax-mulcom 9046  ax-addass 9047  ax-mulass 9048  ax-distr 9049  ax-i2m1 9050  ax-1ne0 9051  ax-1rid 9052  ax-rnegex 9053  ax-rrecex 9054  ax-cnre 9055  ax-pre-lttri 9056  ax-pre-lttrn 9057  ax-pre-ltadd 9058  ax-pre-mulgt0 9059
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2702  df-rex 2703  df-reu 2704  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-uni 4008  df-iun 4087  df-br 4205  df-opab 4259  df-mpt 4260  df-tr 4295  df-eprel 4486  df-id 4490  df-po 4495  df-so 4496  df-fr 4533  df-we 4535  df-ord 4576  df-on 4577  df-lim 4578  df-suc 4579  df-om 4838  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-fv 5454  df-ov 6076  df-oprab 6077  df-mpt2 6078  df-1st 6341  df-2nd 6342  df-riota 6541  df-recs 6625  df-rdg 6660  df-er 6897  df-en 7102  df-dom 7103  df-sdom 7104  df-pnf 9114  df-mnf 9115  df-xr 9116  df-ltxr 9117  df-le 9118  df-sub 9285  df-neg 9286  df-nn 9993  df-n0 10214  df-z 10275  df-uz 10481  df-fz 11036
  Copyright terms: Public domain W3C validator