Theorem elfznn0 13557

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

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5102  (class class class)co 7369  0cc0 11044   ≤ cle 11185  ℕ₀cn0 12418  ...cfz 13444

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 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-cnex 11100  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120  ax-pre-mulgt0 11121

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-om 7823  df-1st 7947  df-2nd 7948  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190  df-sub 11383  df-neg 11384  df-nn 12163  df-n0 12419  df-z 12506  df-uz 12770  df-fz 13445

This theorem is referenced by:  fz0ssnn0  13559  fz0fzdiffz0  13574  difelfzle  13578  bcrpcl  14249  bccmpl  14250  bcp1n  14257  bcp1nk  14258  bcval5  14259  permnn  14267  pfxmpt  14619  pfxfv  14623  pfxlen  14624  addlenpfx  14632  pfxswrd  14647  swrdpfx  14648  pfxpfx  14649  pfxpfxid  14650  swrdccatin1  14666  pfxccat3  14675  pfxccatpfx1  14677  pfxccat3a  14679  swrdccat3blem  14680  splfv2a  14697  repswpfx  14726  2cshwcshw  14767  cshwcsh2id  14770  pfxco  14780  binomlem  15771  binom1p  15773  binom1dif  15775  bcxmas  15777  climcnds  15793  arisum  15802  arisum2  15803  pwdif  15810  geolim  15812  geo2sum  15815  mertenslem1  15826  mertenslem2  15827  mertens  15828  risefacval2  15952  fallfacval2  15953  fallfacval3  15954  risefaccllem  15955  fallfaccllem  15956  risefacp1  15971  fallfacp1  15972  fallfacfwd  15978  binomfallfaclem1  15981  binomfallfaclem2  15982  binomrisefac  15984  bcfallfac  15986  bpolylem  15990  bpolysum  15995  bpolydiflem  15996  fsumkthpow  15998  bpoly4  16001  efcvgfsum  16028  efcj  16034  efaddlem  16035  effsumlt  16055  eirrlem  16148  3dvds  16277  pwp1fsum  16337  prmdiveq  16732  hashgcdlem  16734  pcbc  16847  vdwapf  16919  vdwlem2  16929  vdwlem6  16933  vdwlem8  16935  psgnunilem2  19409  efgcpbllemb  19669  srgbinomlem3  20148  srgbinomlem4  20149  srgbinomlem  20150  freshmansdream  21516  coe1mul2  22188  coe1tmmul2  22195  coe1tmmul  22196  cply1mul  22216  gsummoncoe1  22228  m2pmfzgsumcl  22668  decpmatmul  22692  pmatcollpw3fi1lem1  22706  mp2pm2mplem4  22729  pm2mpmhmlem2  22739  chpscmatgsumbin  22764  chpscmatgsummon  22765  chfacfscmulgsum  22780  chfacfpmmulgsum  22784  cpmadugsumlemB  22794  cpmadugsumlemC  22795  cpmadugsumlemF  22796  cpmadugsumfi  22797  mbfi1fseqlem3  25651  mbfi1fseqlem4  25652  itg0  25714  itgz  25715  itgcl  25718  iblabsr  25764  iblmulc2  25765  itgsplit  25770  dvn2bss  25865  coe1mul3  26037  elply2  26134  plyf  26136  elplyd  26140  ply1termlem  26141  plyeq0lem  26148  plypf1  26150  plyaddlem1  26151  plymullem1  26152  plyaddlem  26153  plymullem  26154  coeeulem  26162  coeidlem  26175  coeid3  26178  plyco  26179  coeeq2  26180  dgreq  26182  coefv0  26186  coeaddlem  26187  coemullem  26188  coemulhi  26192  coemulc  26193  coe1termlem  26196  plycn  26199  plycnOLD  26200  plycjlem  26215  plycj  26216  plycjOLD  26218  plyrecj  26220  dvply1  26224  dvply2g  26225  dvply2gOLD  26226  vieta1lem2  26252  elqaalem2  26261  elqaalem3  26262  aareccl  26267  aalioulem1  26273  taylply2  26308  taylply2OLD  26309  taylply  26310  dvtaylp  26311  dvntaylp0  26313  taylthlem2  26315  taylthlem2OLD  26316  pserulm  26364  psercn2  26365  psercn2OLD  26366  pserdvlem2  26371  abelthlem6  26379  abelthlem7  26381  abelthlem8  26382  advlogexp  26597  cxpeq  26700  log2tlbnd  26888  log2ublem2  26890  log2ub  26892  birthdaylem2  26895  birthdaylem3  26896  ftalem1  27016  ftalem5  27020  basellem2  27025  basellem3  27026  dvdsppwf1o  27129  musum  27134  sgmppw  27141  1sgmprm  27143  logexprlim  27169  mersenne  27171  lgseisenlem1  27319  dchrisum0flblem1  27452  pntpbnd2  27531  crctcshwlkn0  29801  bcm1n  32768  plymulx0  34531  signsplypnf  34534  signstres  34559  subfacval2  35167  subfaclim  35168  cvmliftlem7  35271  bccolsum  35719  knoppcnlem7  36480  knoppcnlem8  36481  knoppndvlem5  36497  knoppndvlem11  36503  knoppndvlem14  36506  knoppndvlem15  36507  poimirlem3  37610  poimirlem4  37611  poimirlem12  37619  poimirlem15  37622  poimirlem16  37623  poimirlem17  37624  poimirlem19  37626  poimirlem20  37627  poimirlem23  37630  poimirlem24  37631  poimirlem25  37632  poimirlem28  37635  poimirlem29  37636  poimirlem31  37638  iblmulc2nc  37672  lcmineqlem1  42010  lcmineqlem2  42011  lcmineqlem3  42012  lcmineqlem4  42013  lcmineqlem6  42015  aks6d1c2lem3  42107  bcled  42159  jm2.22  42977  jm2.23  42978  hbt  43112  cnsrplycl  43149  bcc0  44322  binomcxplemnn0  44331  binomcxplemfrat  44333  binomcxplemradcnv  44334  dvnmptdivc  45929  dvnmul  45934  dvnprodlem1  45937  dvnprodlem2  45938  dvnprodlem3  45939  iblsplit  45957  elaa2lem  46224  etransclem2  46227  etransclem23  46248  etransclem28  46253  etransclem29  46254  etransclem32  46257  etransclem33  46258  etransclem35  46260  etransclem38  46263  etransclem39  46264  etransclem43  46268  etransclem44  46269  etransclem45  46270  etransclem46  46271  etransclem47  46272  etransclem48  46273  2elfz3nn0  47310  fz0addcom  47311  2elfz2melfz  47312  fz0addge0  47313  fmtnorec2lem  47536  fmtnodvds  47538  fmtnorec3  47542  lighneallem3  47601  lighneallem4b  47603  lighneallem4  47604  altgsumbc  48333  altgsumbcALT  48334  ply1mulgsumlem2  48369  ply1mulgsum  48372  nn0sumshdiglemA  48601  nn0sumshdiglemB  48602  aacllem  49783