Theorem elfzuz3 13424

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

Syntax hints:   → wi 4   ∈ wcel 2109  ‘cfv 6482  (class class class)co 7349  ℤ_≥cuz 12735  ...cfz 13410

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 5235  ax-nul 5245  ax-pr 5371  ax-un 7671  ax-cnex 11065  ax-resscn 11066

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-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-fv 6490  df-ov 7352  df-oprab 7353  df-mpo 7354  df-1st 7924  df-2nd 7925  df-neg 11350  df-z 12472  df-uz 12736  df-fz 13411

This theorem is referenced by:  elfzel2  13425  elfzle2  13431  peano2fzr  13440  fzsplit2  13452  fzsplit  13453  fznn0sub  13459  fzopth  13464  fzss1  13466  fzss2  13467  fzp1elp1  13480  predfz  13556  fzosplit  13595  fzoend  13660  fzofzp1b  13668  uzindi  13889  seqcl2  13927  seqfveq2  13931  monoord  13939  sermono  13941  seqsplit  13942  seqf1olem2  13949  seqid2  13955  seqhomo  13956  seqz  13957  bcval5  14225  seqcoll  14371  seqcoll2  14372  swrdval2  14553  pfxres  14586  pfxf  14587  spllen  14660  splfv2a  14662  repswpfx  14691  fsum0diag2  15690  climcndslem2  15757  prodfn0  15801  lcmflefac  16559  pcbc  16812  vdwlem2  16894  vdwlem5  16897  vdwlem6  16898  vdwlem8  16900  prmgaplem1  16961  psgnunilem5  19373  efgsres  19617  efgredleme  19622  efgcpbllemb  19634  imasdsf1olem  24259  volsup  25455  dvn2bss  25830  dvtaylp  26276  wilth  26979  ftalem1  26981  ppisval2  27013  dvdsppwf1o  27094  logfaclbnd  27131  bposlem6  27198  wlkres  29614  fzsplit3  32737  wrdres  32877  pfxf1  32884  swrdrn2  32897  swrdrn3  32898  swrdf1  32899  swrdrndisj  32900  splfv3  32901  pfxchn  32952  cycpmco2f1  33067  cycpmco2rn  33068  cycpmco2lem7  33075  ballotlemsima  34490  ballotlemfrc  34501  ballotlemfrceq  34503  fzssfzo  34513  signstres  34549  fsum2dsub  34581  revpfxsfxrev  35099  swrdrevpfx  35100  pfxwlk  35107  erdszelem7  35180  erdszelem8  35181  poimirlem1  37611  poimirlem2  37612  poimirlem3  37613  poimirlem4  37614  poimirlem7  37617  poimirlem12  37622  poimirlem15  37625  poimirlem16  37626  poimirlem17  37627  poimirlem19  37629  poimirlem20  37630  poimirlem23  37633  poimirlem24  37634  poimirlem25  37635  poimirlem29  37639  poimirlem31  37641  mettrifi  37747  fzsplitnd  41965  aks6d1c2lem4  42110  bcc0  44323  iunincfi  45082  monoordxrv  45470  fmulcl  45572  fmul01lt1lem2  45576  dvnprodlem2  45938  stoweidlem11  46002  stoweidlem17  46008  fourierdlem15  46113  ssfz12  47308  smonoord  47365