Theorem elfzuz3 12908

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

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6357  (class class class)co 7158  ℤ_≥cuz 12246  ...cfz 12895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-cnex 10595  ax-resscn 10596

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-iun 4923  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-fv 6365  df-ov 7161  df-oprab 7162  df-mpo 7163  df-1st 7691  df-2nd 7692  df-neg 10875  df-z 11985  df-uz 12247  df-fz 12896

This theorem is referenced by:  elfzel2  12909  elfzle2  12914  peano2fzr  12923  fzsplit2  12935  fzsplit  12936  fznn0sub  12942  fzopth  12947  fzss1  12949  fzss2  12950  fzp1elp1  12963  predfz  13035  fzosplit  13073  fzoend  13131  fzofzp1b  13138  uzindi  13353  seqcl2  13391  seqfveq2  13395  monoord  13403  sermono  13405  seqsplit  13406  seqf1olem2  13413  seqid2  13419  seqhomo  13420  seqz  13421  bcval5  13681  seqcoll  13825  seqcoll2  13826  swrdval2  14010  pfxres  14043  pfxf  14044  spllen  14118  splfv2a  14120  repswpfx  14149  fsum0diag2  15140  climcndslem2  15207  prodfn0  15252  lcmflefac  15994  pcbc  16238  vdwlem2  16320  vdwlem5  16323  vdwlem6  16324  vdwlem8  16326  prmgaplem1  16387  psgnunilem5  18624  efgsres  18866  efgredleme  18871  efgcpbllemb  18883  imasdsf1olem  22985  volsup  24159  dvn2bss  24529  dvtaylp  24960  wilth  25650  ftalem1  25652  ppisval2  25684  dvdsppwf1o  25765  logfaclbnd  25800  bposlem6  25867  wlkres  27454  fzsplit3  30519  wrdres  30615  pfxf1  30620  swrdrn2  30630  swrdrn3  30631  swrdf1  30632  swrdrndisj  30633  splfv3  30634  cycpmco2f1  30768  cycpmco2rn  30769  cycpmco2lem7  30776  ballotlemsima  31775  ballotlemfrc  31786  ballotlemfrceq  31788  fzssfzo  31811  signstres  31847  fsum2dsub  31880  revpfxsfxrev  32364  swrdrevpfx  32365  pfxwlk  32372  erdszelem7  32446  erdszelem8  32447  poimirlem1  34895  poimirlem2  34896  poimirlem3  34897  poimirlem4  34898  poimirlem7  34901  poimirlem12  34906  poimirlem15  34909  poimirlem16  34910  poimirlem17  34911  poimirlem19  34913  poimirlem20  34914  poimirlem23  34917  poimirlem24  34918  poimirlem25  34919  poimirlem29  34923  poimirlem31  34925  mettrifi  35034  bcc0  40679  iunincfi  41367  monoordxrv  41765  fmulcl  41869  fmul01lt1lem2  41873  dvnprodlem2  42239  stoweidlem11  42303  stoweidlem17  42309  fourierdlem15  42414  ssfz12  43521  smonoord  43538