Theorem elfznn0 12994

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 12992	. 2 ⊢ (𝐾 ∈ (0...𝑁) ↔ (𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁))
2	1	simp1bi 1141	1 ⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2110   class class class wbr 5058  (class class class)co 7150  0cc0 10531   ≤ cle 10670  ℕ₀cn0 11891  ...cfz 12886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-tp 4565  df-op 4567  df-uni 4832  df-iun 4913  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7575  df-1st 7683  df-2nd 7684  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-er 8283  df-en 8504  df-dom 8505  df-sdom 8506  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-nn 11633  df-n0 11892  df-z 11976  df-uz 12238  df-fz 12887

This theorem is referenced by:  fz0ssnn0  12996  fz0fzdiffz0  13010  difelfzle  13014  bcrpcl  13662  bccmpl  13663  bcp1n  13670  bcp1nk  13671  bcval5  13672  permnn  13680  pfxmpt  14034  pfxfv  14038  pfxlen  14039  addlenpfx  14047  pfxswrd  14062  swrdpfx  14063  pfxpfx  14064  pfxpfxid  14065  swrdccatin1  14081  pfxccat3  14090  pfxccatpfx1  14092  pfxccat3a  14094  swrdccat3blem  14095  splfv2a  14112  repswpfx  14141  2cshwcshw  14181  cshwcsh2id  14184  pfxco  14194  binomlem  15178  binom1p  15180  binom1dif  15182  bcxmas  15184  climcnds  15200  arisum  15209  arisum2  15210  pwdif  15217  pwm1geoserOLD  15219  geolim  15220  geo2sum  15223  mertenslem1  15234  mertenslem2  15235  mertens  15236  risefacval2  15358  fallfacval2  15359  fallfacval3  15360  risefaccllem  15361  fallfaccllem  15362  risefacp1  15377  fallfacp1  15378  fallfacfwd  15384  binomfallfaclem1  15387  binomfallfaclem2  15388  binomrisefac  15390  bcfallfac  15392  bpolylem  15396  bpolysum  15401  bpolydiflem  15402  fsumkthpow  15404  bpoly4  15407  efcvgfsum  15433  efcj  15439  efaddlem  15440  effsumlt  15458  eirrlem  15551  3dvds  15674  pwp1fsum  15736  prmdiveq  16117  hashgcdlem  16119  pcbc  16230  vdwapf  16302  vdwlem2  16312  vdwlem6  16316  vdwlem8  16318  psgnunilem2  18617  efgcpbllemb  18875  srgbinomlem3  19286  srgbinomlem4  19287  srgbinomlem  19288  coe1mul2  20431  coe1tmmul2  20438  coe1tmmul  20439  cply1mul  20456  gsummoncoe1  20466  m2pmfzgsumcl  21350  decpmatmul  21374  pmatcollpw3fi1lem1  21388  mp2pm2mplem4  21411  pm2mpmhmlem2  21421  chpscmatgsumbin  21446  chpscmatgsummon  21447  chfacfscmulgsum  21462  chfacfpmmulgsum  21466  cpmadugsumlemB  21476  cpmadugsumlemC  21477  cpmadugsumlemF  21478  cpmadugsumfi  21479  mbfi1fseqlem3  24312  mbfi1fseqlem4  24313  itg0  24374  itgz  24375  itgcl  24378  iblabsr  24424  iblmulc2  24425  itgsplit  24430  dvn2bss  24521  coe1mul3  24687  elply2  24780  plyf  24782  elplyd  24786  ply1termlem  24787  plyeq0lem  24794  plypf1  24796  plyaddlem1  24797  plymullem1  24798  plyaddlem  24799  plymullem  24800  coeeulem  24808  coeidlem  24821  coeid3  24824  plyco  24825  coeeq2  24826  dgreq  24828  coefv0  24832  coeaddlem  24833  coemullem  24834  coemulhi  24838  coemulc  24839  coe1termlem  24842  plycn  24845  plycjlem  24860  plycj  24861  plyrecj  24863  dvply1  24867  dvply2g  24868  vieta1lem2  24894  elqaalem2  24903  elqaalem3  24904  aareccl  24909  aalioulem1  24915  taylply2  24950  taylply  24951  dvtaylp  24952  dvntaylp0  24954  taylthlem2  24956  pserulm  25004  psercn2  25005  pserdvlem2  25010  abelthlem6  25018  abelthlem7  25020  abelthlem8  25021  advlogexp  25232  cxpeq  25332  log2tlbnd  25517  log2ublem2  25519  log2ub  25521  birthdaylem2  25524  birthdaylem3  25525  ftalem1  25644  ftalem5  25648  basellem2  25653  basellem3  25654  dvdsppwf1o  25757  musum  25762  sgmppw  25767  1sgmprm  25769  logexprlim  25795  mersenne  25797  lgseisenlem1  25945  dchrisum0flblem1  26078  pntpbnd2  26157  crctcshwlkn0  27593  bcm1n  30512  freshmansdream  30854  plymulx0  31812  signsplypnf  31815  signstres  31840  subfacval2  32429  subfaclim  32430  cvmliftlem7  32533  bccolsum  32966  knoppcnlem7  33833  knoppcnlem8  33834  knoppndvlem5  33850  knoppndvlem11  33856  knoppndvlem14  33859  knoppndvlem15  33860  poimirlem3  34889  poimirlem4  34890  poimirlem12  34898  poimirlem15  34901  poimirlem16  34902  poimirlem17  34903  poimirlem19  34905  poimirlem20  34906  poimirlem23  34909  poimirlem24  34910  poimirlem25  34911  poimirlem28  34914  poimirlem29  34915  poimirlem31  34917  iblmulc2nc  34951  jm2.22  39585  jm2.23  39586  hbt  39723  cnsrplycl  39760  bcc0  40665  binomcxplemnn0  40674  binomcxplemfrat  40676  binomcxplemradcnv  40677  dvnmptdivc  42216  dvnmul  42221  dvnprodlem1  42224  dvnprodlem2  42225  dvnprodlem3  42226  iblsplit  42244  elaa2lem  42512  etransclem2  42515  etransclem23  42536  etransclem28  42541  etransclem29  42542  etransclem32  42545  etransclem33  42546  etransclem35  42548  etransclem38  42551  etransclem39  42552  etransclem43  42556  etransclem44  42557  etransclem45  42558  etransclem46  42559  etransclem47  42560  etransclem48  42561  2elfz3nn0  43510  fz0addcom  43511  2elfz2melfz  43512  fz0addge0  43513  fmtnorec2lem  43698  fmtnodvds  43700  fmtnorec3  43704  lighneallem3  43766  lighneallem4b  43768  lighneallem4  43769  altgsumbc  44394  altgsumbcALT  44395  ply1mulgsumlem2  44435  ply1mulgsum  44438  nn0sumshdiglemA  44673  nn0sumshdiglemB  44674  aacllem  44896