Theorem elfzuz3 13553

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2143  ‘cfv 6536  (class class class)co 7410  ℤ_≥cuz 12866  ...cfz 13539

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404  ax-un 7732  ax-cnex 11160  ax-resscn 11161

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544  df-ov 7413  df-oprab 7414  df-mpo 7415  df-1st 7982  df-2nd 7983  df-neg 11448  df-z 12596  df-uz 12867  df-fz 13540

This theorem is used by:  elfzel2  13554  elfzle2  13560  peano2fzr  13569  fzsplit2  13582  fzsplit  13583  fznn0sub  13589  fzopth  13594  fzss1  13596  fzss2  13597  fzp1elp1  13610  predfz  13686  fzosplit  13726  fzoend  13791  fzofzp1b  13799  uzindi  14023  seqcl2  14061  seqfveq2  14065  monoord  14073  sermono  14075  seqsplit  14076  seqf1olem2  14083  seqid2  14089  seqhomo  14090  seqz  14091  bcval5  14359  seqcoll  14506  seqcoll2  14507  swrdval2  14689  pfxres  14722  pfxf  14723  spllen  14796  splfv2a  14798  repswpfx  14827  fsum0diag2  15839  climcndslem2  15909  prodfn0  15953  lcmflefac  16710  pcbc  16964  vdwlem2  17046  vdwlem5  17049  vdwlem6  17050  vdwlem8  17052  prmgaplem1  17113  pfxchn  18670  psgnunilem5  19568  efgsres  19812  efgredleme  19817  efgcpbllemb  19829  imasdsf1olem  24539  volsup  25724  dvn2bss  26098  dvtaylp  26542  wilth  27244  ftalem1  27246  ppisval2  27278  dvdsppwf1o  27359  logfaclbnd  27395  bposlem6  27462  wlkres  30027  fzsplit3  33147  wrdres  33264  pfxf1  33271  swrdrn2  33283  swrdrn3  33284  swrdf1  33285  swrdrndisj  33286  splfv3  33287  cycpmco2f1  33453  cycpmco2rn  33454  cycpmco2lem7  33461  ballotlemsima  34915  ballotlemfrc  34926  ballotlemfrceq  34928  fzssfzo  34938  signstres  34971  fsum2dsub  35003  revpfxsfxrev  35615  swrdrevpfx  35616  pfxwlk  35624  erdszelem7  35697  erdszelem8  35698  poimirlem1  38300  poimirlem2  38301  poimirlem3  38302  poimirlem4  38303  poimirlem7  38306  poimirlem12  38311  poimirlem15  38314  poimirlem16  38315  poimirlem17  38316  poimirlem19  38318  poimirlem20  38319  poimirlem23  38322  poimirlem24  38323  poimirlem25  38324  poimirlem29  38328  poimirlem31  38330  mettrifi  38436  fzsplitnd  42777  aks6d1c2lem4  42922  bcc0  45078  iunincfi  45840  monoordxrv  46223  fmulcl  46325  fmul01lt1lem2  46329  dvnprodlem2  46689  stoweidlem11  46753  stoweidlem17  46759  fourierdlem15  46864  ssfz12  48079  smonoord  48142