Theorem elfzuz3 13451

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 13448	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)))
2	1	simprbi 497	1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾))

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6502  (class class class)co 7370  ℤ_≥cuz 12765  ...cfz 13437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5245  ax-nul 5255  ax-pr 5381  ax-un 7692  ax-cnex 11096  ax-resscn 11097

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5529  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-fv 6510  df-ov 7373  df-oprab 7374  df-mpo 7375  df-1st 7945  df-2nd 7946  df-neg 11381  df-z 12503  df-uz 12766  df-fz 13438

This theorem is referenced by:  elfzel2  13452  elfzle2  13458  peano2fzr  13467  fzsplit2  13479  fzsplit  13480  fznn0sub  13486  fzopth  13491  fzss1  13493  fzss2  13494  fzp1elp1  13507  predfz  13583  fzosplit  13622  fzoend  13687  fzofzp1b  13695  uzindi  13919  seqcl2  13957  seqfveq2  13961  monoord  13969  sermono  13971  seqsplit  13972  seqf1olem2  13979  seqid2  13985  seqhomo  13986  seqz  13987  bcval5  14255  seqcoll  14401  seqcoll2  14402  swrdval2  14584  pfxres  14617  pfxf  14618  spllen  14691  splfv2a  14693  repswpfx  14722  fsum0diag2  15720  climcndslem2  15787  prodfn0  15831  lcmflefac  16589  pcbc  16842  vdwlem2  16924  vdwlem5  16927  vdwlem6  16928  vdwlem8  16930  prmgaplem1  16991  pfxchn  18547  psgnunilem5  19440  efgsres  19684  efgredleme  19689  efgcpbllemb  19701  imasdsf1olem  24334  volsup  25530  dvn2bss  25905  dvtaylp  26351  wilth  27054  ftalem1  27056  ppisval2  27088  dvdsppwf1o  27169  logfaclbnd  27206  bposlem6  27273  wlkres  29760  fzsplit3  32890  wrdres  33034  pfxf1  33041  swrdrn2  33053  swrdrn3  33054  swrdf1  33055  swrdrndisj  33056  splfv3  33057  cycpmco2f1  33224  cycpmco2rn  33225  cycpmco2lem7  33232  ballotlemsima  34700  ballotlemfrc  34711  ballotlemfrceq  34713  fzssfzo  34723  signstres  34759  fsum2dsub  34791  revpfxsfxrev  35338  swrdrevpfx  35339  pfxwlk  35346  erdszelem7  35419  erdszelem8  35420  poimirlem1  37901  poimirlem2  37902  poimirlem3  37903  poimirlem4  37904  poimirlem7  37907  poimirlem12  37912  poimirlem15  37915  poimirlem16  37916  poimirlem17  37917  poimirlem19  37919  poimirlem20  37920  poimirlem23  37923  poimirlem24  37924  poimirlem25  37925  poimirlem29  37929  poimirlem31  37931  mettrifi  38037  fzsplitnd  42381  aks6d1c2lem4  42526  bcc0  44725  iunincfi  45482  monoordxrv  45868  fmulcl  45970  fmul01lt1lem2  45974  dvnprodlem2  46334  stoweidlem11  46398  stoweidlem17  46404  fourierdlem15  46509  ssfz12  47703  smonoord  47760