Theorem elfzuz3 13666

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ‘cfv 6547  (class class class)co 7430  ℤ_≥cuz 12978  ...cfz 13652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395  ax-un 7761  ax-cnex 11269  ax-resscn 11270

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  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 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6501  df-fun 6549  df-fn 6550  df-f 6551  df-fv 6555  df-ov 7433  df-oprab 7434  df-mpo 7435  df-1st 8011  df-2nd 8012  df-neg 11557  df-z 12707  df-uz 12979  df-fz 13653

This theorem is used by:  elfzel2  13667  elfzle2  13674  peano2fzr  13683  fzsplit2  13696  fzsplit  13697  fznn0sub  13703  fzopth  13708  fzss1  13710  fzss2  13711  fzp1elp1  13724  predfz  13800  fzosplit  13840  fzoend  13905  fzofzp1b  13913  uzindi  14138  seqcl2  14176  seqfveq2  14180  monoord  14188  sermono  14190  seqsplit  14191  seqf1olem2  14198  seqid2  14204  seqhomo  14205  seqz  14206  bcval5  14475  seqcoll  14622  seqcoll2  14623  swrdval2  14808  swrdf1  14813  swrdrn3  14816  pfxres  14843  pfxf  14844  spllen  14917  splfv2a  14919  revpfxsfxrev  14931  swrdrevpfx  14932  repswpfx  14950  fsum0diag2  15964  climcndslem2  16034  prodfn0  16078  lcmflefac  16838  pcbc  17093  vdwlem2  17175  vdwlem5  17178  vdwlem6  17179  vdwlem8  17181  prmgaplem1  17242  pfxchn  18799  psgnunilem5  19723  efgsres  19967  efgredleme  19972  efgcpbllemb  19984  imasdsf1olem  24707  volsup  25892  dvn2bss  26265  dvtaylp  26712  wilth  27413  ftalem1  27415  ppisval2  27447  dvdsppwf1o  27528  logfaclbnd  27564  bposlem6  27631  wlkres  30264  pfxwlk  30281  fzsplit3  33441  wrdres  33558  pfxf1  33565  swrdrn2  33573  swrdrndisj  33574  splfv3  33575  cycpmco2f1  33741  cycpmco2rn  33742  cycpmco2lem7  33749  ballotlemsima  35204  ballotlemfrc  35215  ballotlemfrceq  35217  fzssfzo  35227  signstres  35260  fsum2dsub  35292  erdszelem7  36086  erdszelem8  36087  poimirlem1  38685  poimirlem2  38686  poimirlem3  38687  poimirlem4  38688  poimirlem7  38691  poimirlem12  38696  poimirlem15  38699  poimirlem16  38700  poimirlem17  38701  poimirlem19  38703  poimirlem20  38704  poimirlem23  38707  poimirlem24  38708  poimirlem25  38709  poimirlem29  38713  poimirlem31  38715  mettrifi  38837  fzsplitnd  43178  aks6d1c2lem4  43323  bcc0  45470  iunincfi  46254  monoordxrv  46636  fmulcl  46738  fmul01lt1lem2  46742  dvnprodlem2  47102  stoweidlem11  47166  stoweidlem17  47172  fourierdlem15  47277  ssfz12  48529  smonoord  48592