Theorem elfznn0 13794

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   class class class wbr 5108  (class class class)co 7451  0cc0 11239   ≤ cle 11383  ℕ₀cn0 12646  ...cfz 13679

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783  ax-cnex 11295  ax-resscn 11296  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-addrcl 11300  ax-mulcl 11301  ax-mulrcl 11302  ax-mulcom 11303  ax-addass 11304  ax-mulass 11305  ax-distr 11306  ax-i2m1 11307  ax-1ne0 11308  ax-1rid 11309  ax-rnegex 11310  ax-rrecex 11311  ax-cnre 11312  ax-pre-lttri 11313  ax-pre-lttrn 11314  ax-pre-ltadd 11315  ax-pre-mulgt0 11316

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-pred 6330  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-riota 7408  df-ov 7454  df-oprab 7455  df-mpo 7456  df-om 7912  df-1st 8035  df-2nd 8036  df-frecs 8337  df-wrecs 8368  df-recs 8417  df-rdg 8456  df-er 8755  df-en 9012  df-dom 9013  df-sdom 9014  df-pnf 11384  df-mnf 11385  df-xr 11386  df-ltxr 11387  df-le 11388  df-sub 11582  df-neg 11583  df-nn 12376  df-n0 12647  df-z 12734  df-uz 13006  df-fz 13680

This theorem is used by:  fz0ssnn0  13796  fz0fzdiffz0  13811  difelfzle  13815  bcrpcl  14493  bccmpl  14494  bcp1n  14501  bcp1nk  14502  bcval5  14503  permnn  14511  pfxmpt  14870  pfxfv  14874  pfxlen  14875  addlenpfx  14882  pfxswrd  14897  swrdpfx  14898  pfxpfx  14899  pfxpfxid  14900  lenrevpfxcctswrd  14903  swrdccatin1  14916  pfxccat3  14925  pfxccatpfx1  14927  pfxccat3a  14929  swrdccat3blem  14930  splfv2a  14947  repswpfx  14978  2cshwcshw  15018  cshwcsh2id  15021  pfxco  15031  binomlem  16042  binom1p  16044  binom1dif  16046  bcxmas  16048  climcnds  16064  arisum  16073  arisum2  16074  pwdif  16081  geolim  16083  geo2sum  16086  mertenslem1  16097  mertenslem2  16098  mertens  16099  risefacval2  16221  fallfacval2  16222  fallfacval3  16223  risefaccllem  16224  fallfaccllem  16225  risefacp1  16239  fallfacp1  16240  fallfacfwd  16246  binomfallfaclem1  16249  binomfallfaclem2  16250  binomrisefac  16252  bcfallfac  16254  bpolylem  16258  bpolysum  16263  bpolydiflem  16264  fsumkthpow  16266  bpoly4  16269  efcvgfsum  16296  efcj  16302  efaddlem  16303  effsumlt  16323  eirrlem  16416  3dvds  16545  pwp1fsum  16605  prmdiveq  17007  hashgcdlem  17009  pcbc  17122  vdwapf  17194  vdwlem2  17204  vdwlem6  17208  vdwlem8  17210  psgnunilem2  19760  efgcpbllemb  20020  srgbinomlem3  20505  srgbinomlem4  20506  srgbinomlem  20507  freshmansdream  21935  coe1mul2  22643  coe1tmmul2  22650  coe1tmmul  22651  cply1mul  22669  gsummoncoe1  22681  m2pmfzgsumcl  23121  decpmatmul  23145  pmatcollpw3fi1lem1  23159  mp2pm2mplem4  23182  pm2mpmhmlem2  23192  chpscmatgsumbin  23217  chpscmatgsummon  23218  chfacfscmulgsum  23233  chfacfpmmulgsum  23237  cpmadugsumlemB  23247  cpmadugsumlemC  23248  cpmadugsumlemF  23249  cpmadugsumfi  23250  mbfi1fseqlem3  26093  mbfi1fseqlem4  26094  itg0  26155  itgz  26156  itgcl  26159  iblabsr  26205  iblmulc2  26206  itgsplit  26211  dvn2bss  26305  coe1mul3  26472  elply2  26569  plyf  26571  elplyd  26575  ply1termlem  26576  plyeq0lem  26584  plypf1  26586  plyaddlem1  26587  plymullem1  26588  plyaddlem  26589  plymullem  26590  coeeulem  26598  coeidlem  26611  coeid3  26614  plyco  26615  coeeq2  26616  dgreq  26618  coefv0  26622  coeaddlem  26623  coemullem  26624  coemulhi  26628  coemulc  26629  coe1termlem  26632  plycn  26635  plycjlem  26650  plycj  26651  plyrecj  26653  plyn0mulidp  26657  dvply1  26660  dvply2g  26661  vieta1lem2  26689  cnsrplycl  26692  elqaalem2  26700  elqaalem3  26701  aareccl  26710  aalioulem1  26716  taylply2  26752  taylply  26753  dvtaylp  26754  dvntaylp0  26756  taylthlem2  26758  pserulm  26806  psercn2  26807  pserdvlem2  26812  abelthlem6  26820  abelthlem7  26822  abelthlem8  26823  advlogexp  27040  cxpeq  27142  log2tlbnd  27330  log2ublem2  27332  log2ub  27334  birthdaylem2  27337  birthdaylem3  27338  ftalem1  27457  ftalem5  27461  basellem2  27466  basellem3  27467  dvdsppwf1o  27570  musum  27575  sgmppw  27581  1sgmprm  27583  logexprlim  27609  mersenne  27611  lgseisenlem1  27759  dchrisum0flblem1  27892  pntpbnd2  27971  crctcshwlkn0  30467  bcm1n  33483  gsummptrev  33716  gsummulsubdishift1  33728  esplyfv1  34312  esplyfv  34313  esplysply  34314  vietalem  34322  vieta  34323  signsplypnf  35290  signstres  35315  subfacval2  36160  subfaclim  36161  cvmliftlem7  36264  bccolsum  36719  knoppcnlem7  37580  knoppcnlem8  37581  knoppndvlem5  37597  knoppndvlem11  37603  knoppndvlem14  37606  knoppndvlem15  37607  poimirlem3  38809  poimirlem4  38810  poimirlem12  38818  poimirlem15  38821  poimirlem16  38822  poimirlem17  38823  poimirlem19  38825  poimirlem20  38826  poimirlem23  38829  poimirlem24  38830  poimirlem25  38831  poimirlem28  38834  poimirlem29  38835  poimirlem31  38837  iblmulc2nc  38871  lcmineqlem1  43345  lcmineqlem2  43346  lcmineqlem3  43347  lcmineqlem4  43348  lcmineqlem6  43350  aks6d1c2lem3  43442  bcled  43494  jm2.22  44268  jm2.23  44269  hbt  44397  bcc0  45585  binomcxplemnn0  45594  binomcxplemfrat  45596  binomcxplemradcnv  45597  dvnmptdivc  47221  dvnmul  47226  dvnprodlem1  47229  dvnprodlem2  47230  dvnprodlem3  47231  iblsplit  47249  elaa2lem  47516  etransclem2  47519  etransclem23  47540  etransclem28  47545  etransclem29  47546  etransclem32  47549  etransclem33  47550  etransclem35  47552  etransclem38  47555  etransclem39  47556  etransclem43  47560  etransclem44  47561  etransclem45  47562  etransclem46  47563  etransclem47  47564  etransclem48  47565  2elfz3nn0  48659  fz0addcom  48660  2elfz2melfz  48661  fz0addge0  48662  facnn0dvdsfac  48728  fmtnorec2lem  48900  fmtnodvds  48902  fmtnorec3  48906  lighneallem3  48965  lighneallem4b  48967  lighneallem4  48968  altgsumbc  49795  altgsumbcALT  49796  ply1mulgsumlem2  49830  ply1mulgsum  49833  nn0sumshdiglemA  50062  nn0sumshdiglemB  50063  aacllem  51367