Theorem elfzuz3 13581

Description: Membership in a finite set of sequential integers implies membership in an upper set of integers. (Contributed by NM, 28-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)

Assertion

Ref	Expression
elfzuz3	⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾))

Proof of Theorem elfzuz3

Step	Hyp	Ref	Expression
1		elfzuzb 13578	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)))
2	1	simprbi 496	1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾))

Syntax hints:   → wi 4   ∈ wcel 2108  ‘cfv 6573  (class class class)co 7448  ℤ_≥cuz 12903  ...cfz 13567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-fv 6581  df-ov 7451  df-oprab 7452  df-mpo 7453  df-1st 8030  df-2nd 8031  df-neg 11523  df-z 12640  df-uz 12904  df-fz 13568

This theorem is referenced by:  elfzel2  13582  elfzle2  13588  peano2fzr  13597  fzsplit2  13609  fzsplit  13610  fznn0sub  13616  fzopth  13621  fzss1  13623  fzss2  13624  fzp1elp1  13637  predfz  13710  fzosplit  13749  fzoend  13807  fzofzp1b  13815  uzindi  14033  seqcl2  14071  seqfveq2  14075  monoord  14083  sermono  14085  seqsplit  14086  seqf1olem2  14093  seqid2  14099  seqhomo  14100  seqz  14101  bcval5  14367  seqcoll  14513  seqcoll2  14514  swrdval2  14694  pfxres  14727  pfxf  14728  spllen  14802  splfv2a  14804  repswpfx  14833  fsum0diag2  15831  climcndslem2  15898  prodfn0  15942  lcmflefac  16695  pcbc  16947  vdwlem2  17029  vdwlem5  17032  vdwlem6  17033  vdwlem8  17035  prmgaplem1  17096  psgnunilem5  19536  efgsres  19780  efgredleme  19785  efgcpbllemb  19797  imasdsf1olem  24404  volsup  25610  dvn2bss  25986  dvtaylp  26430  wilth  27132  ftalem1  27134  ppisval2  27166  dvdsppwf1o  27247  logfaclbnd  27284  bposlem6  27351  wlkres  29706  fzsplit3  32799  wrdres  32901  pfxf1  32908  swrdrn2  32921  swrdrn3  32922  swrdf1  32923  swrdrndisj  32924  splfv3  32925  pfxchn  32982  cycpmco2f1  33117  cycpmco2rn  33118  cycpmco2lem7  33125  ballotlemsima  34480  ballotlemfrc  34491  ballotlemfrceq  34493  fzssfzo  34516  signstres  34552  fsum2dsub  34584  revpfxsfxrev  35083  swrdrevpfx  35084  pfxwlk  35091  erdszelem7  35165  erdszelem8  35166  poimirlem1  37581  poimirlem2  37582  poimirlem3  37583  poimirlem4  37584  poimirlem7  37587  poimirlem12  37592  poimirlem15  37595  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem23  37603  poimirlem24  37604  poimirlem25  37605  poimirlem29  37609  poimirlem31  37611  mettrifi  37717  fzsplitnd  41939  aks6d1c2lem4  42084  bcc0  44309  iunincfi  44996  monoordxrv  45397  fmulcl  45502  fmul01lt1lem2  45506  dvnprodlem2  45868  stoweidlem11  45932  stoweidlem17  45938  fourierdlem15  46043  ssfz12  47229  smonoord  47245