Theorem elfznn0 13642

Description: A member of a finite set of sequential nonnegative integers is a nonnegative integer. (Contributed by NM, 5-Aug-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)

Assertion

Ref	Expression
elfznn0	⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈ ℕ0)

Proof of Theorem elfznn0

Step	Hyp	Ref	Expression
1		elfz2nn0 13640	. 2 ⊢ (𝐾 ∈ (0...𝑁) ↔ (𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁))
2	1	simp1bi 1145	1 ⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5124  (class class class)co 7410  0cc0 11134   ≤ cle 11275  ℕ₀cn0 12506  ...cfz 13529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734  ax-cnex 11190  ax-resscn 11191  ax-1cn 11192  ax-icn 11193  ax-addcl 11194  ax-addrcl 11195  ax-mulcl 11196  ax-mulrcl 11197  ax-mulcom 11198  ax-addass 11199  ax-mulass 11200  ax-distr 11201  ax-i2m1 11202  ax-1ne0 11203  ax-1rid 11204  ax-rnegex 11205  ax-rrecex 11206  ax-cnre 11207  ax-pre-lttri 11208  ax-pre-lttrn 11209  ax-pre-ltadd 11210  ax-pre-mulgt0 11211

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-iun 4974  df-br 5125  df-opab 5187  df-mpt 5207  df-tr 5235  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6295  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7867  df-1st 7993  df-2nd 7994  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-er 8724  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11276  df-mnf 11277  df-xr 11278  df-ltxr 11279  df-le 11280  df-sub 11473  df-neg 11474  df-nn 12246  df-n0 12507  df-z 12594  df-uz 12858  df-fz 13530

This theorem is referenced by:  fz0ssnn0  13644  fz0fzdiffz0  13659  difelfzle  13663  bcrpcl  14331  bccmpl  14332  bcp1n  14339  bcp1nk  14340  bcval5  14341  permnn  14349  pfxmpt  14701  pfxfv  14705  pfxlen  14706  addlenpfx  14714  pfxswrd  14729  swrdpfx  14730  pfxpfx  14731  pfxpfxid  14732  swrdccatin1  14748  pfxccat3  14757  pfxccatpfx1  14759  pfxccat3a  14761  swrdccat3blem  14762  splfv2a  14779  repswpfx  14808  2cshwcshw  14849  cshwcsh2id  14852  pfxco  14862  binomlem  15850  binom1p  15852  binom1dif  15854  bcxmas  15856  climcnds  15872  arisum  15881  arisum2  15882  pwdif  15889  geolim  15891  geo2sum  15894  mertenslem1  15905  mertenslem2  15906  mertens  15907  risefacval2  16031  fallfacval2  16032  fallfacval3  16033  risefaccllem  16034  fallfaccllem  16035  risefacp1  16050  fallfacp1  16051  fallfacfwd  16057  binomfallfaclem1  16060  binomfallfaclem2  16061  binomrisefac  16063  bcfallfac  16065  bpolylem  16069  bpolysum  16074  bpolydiflem  16075  fsumkthpow  16077  bpoly4  16080  efcvgfsum  16107  efcj  16113  efaddlem  16114  effsumlt  16134  eirrlem  16227  3dvds  16355  pwp1fsum  16415  prmdiveq  16810  hashgcdlem  16812  pcbc  16925  vdwapf  16997  vdwlem2  17007  vdwlem6  17011  vdwlem8  17013  psgnunilem2  19481  efgcpbllemb  19741  srgbinomlem3  20193  srgbinomlem4  20194  srgbinomlem  20195  freshmansdream  21540  coe1mul2  22211  coe1tmmul2  22218  coe1tmmul  22219  cply1mul  22239  gsummoncoe1  22251  m2pmfzgsumcl  22691  decpmatmul  22715  pmatcollpw3fi1lem1  22729  mp2pm2mplem4  22752  pm2mpmhmlem2  22762  chpscmatgsumbin  22787  chpscmatgsummon  22788  chfacfscmulgsum  22803  chfacfpmmulgsum  22807  cpmadugsumlemB  22817  cpmadugsumlemC  22818  cpmadugsumlemF  22819  cpmadugsumfi  22820  mbfi1fseqlem3  25675  mbfi1fseqlem4  25676  itg0  25738  itgz  25739  itgcl  25742  iblabsr  25788  iblmulc2  25789  itgsplit  25794  dvn2bss  25889  coe1mul3  26061  elply2  26158  plyf  26160  elplyd  26164  ply1termlem  26165  plyeq0lem  26172  plypf1  26174  plyaddlem1  26175  plymullem1  26176  plyaddlem  26177  plymullem  26178  coeeulem  26186  coeidlem  26199  coeid3  26202  plyco  26203  coeeq2  26204  dgreq  26206  coefv0  26210  coeaddlem  26211  coemullem  26212  coemulhi  26216  coemulc  26217  coe1termlem  26220  plycn  26223  plycnOLD  26224  plycjlem  26239  plycj  26240  plycjOLD  26242  plyrecj  26244  dvply1  26248  dvply2g  26249  dvply2gOLD  26250  vieta1lem2  26276  elqaalem2  26285  elqaalem3  26286  aareccl  26291  aalioulem1  26297  taylply2  26332  taylply2OLD  26333  taylply  26334  dvtaylp  26335  dvntaylp0  26337  taylthlem2  26339  taylthlem2OLD  26340  pserulm  26388  psercn2  26389  psercn2OLD  26390  pserdvlem2  26395  abelthlem6  26403  abelthlem7  26405  abelthlem8  26406  advlogexp  26621  cxpeq  26724  log2tlbnd  26912  log2ublem2  26914  log2ub  26916  birthdaylem2  26919  birthdaylem3  26920  ftalem1  27040  ftalem5  27044  basellem2  27049  basellem3  27050  dvdsppwf1o  27153  musum  27158  sgmppw  27165  1sgmprm  27167  logexprlim  27193  mersenne  27195  lgseisenlem1  27343  dchrisum0flblem1  27476  pntpbnd2  27555  crctcshwlkn0  29808  bcm1n  32777  plymulx0  34584  signsplypnf  34587  signstres  34612  subfacval2  35214  subfaclim  35215  cvmliftlem7  35318  bccolsum  35761  knoppcnlem7  36522  knoppcnlem8  36523  knoppndvlem5  36539  knoppndvlem11  36545  knoppndvlem14  36548  knoppndvlem15  36549  poimirlem3  37652  poimirlem4  37653  poimirlem12  37661  poimirlem15  37664  poimirlem16  37665  poimirlem17  37666  poimirlem19  37668  poimirlem20  37669  poimirlem23  37672  poimirlem24  37673  poimirlem25  37674  poimirlem28  37677  poimirlem29  37678  poimirlem31  37680  iblmulc2nc  37714  lcmineqlem1  42047  lcmineqlem2  42048  lcmineqlem3  42049  lcmineqlem4  42050  lcmineqlem6  42052  aks6d1c2lem3  42144  bcled  42196  jm2.22  42994  jm2.23  42995  hbt  43129  cnsrplycl  43166  bcc0  44339  binomcxplemnn0  44348  binomcxplemfrat  44350  binomcxplemradcnv  44351  dvnmptdivc  45947  dvnmul  45952  dvnprodlem1  45955  dvnprodlem2  45956  dvnprodlem3  45957  iblsplit  45975  elaa2lem  46242  etransclem2  46245  etransclem23  46266  etransclem28  46271  etransclem29  46272  etransclem32  46275  etransclem33  46276  etransclem35  46278  etransclem38  46281  etransclem39  46282  etransclem43  46286  etransclem44  46287  etransclem45  46288  etransclem46  46289  etransclem47  46290  etransclem48  46291  2elfz3nn0  47325  fz0addcom  47326  2elfz2melfz  47327  fz0addge0  47328  fmtnorec2lem  47536  fmtnodvds  47538  fmtnorec3  47542  lighneallem3  47601  lighneallem4b  47603  lighneallem4  47604  altgsumbc  48307  altgsumbcALT  48308  ply1mulgsumlem2  48343  ply1mulgsum  48346  nn0sumshdiglemA  48579  nn0sumshdiglemB  48580  aacllem  49645