Theorem elfzuz3 13562

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

Syntax hints:   → wi 4   ∈ wcel 2107  ‘cfv 6560  (class class class)co 7432  ℤ_≥cuz 12879  ...cfz 13548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431  ax-un 7756  ax-cnex 11212  ax-resscn 11213

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-id 5577  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-fv 6568  df-ov 7435  df-oprab 7436  df-mpo 7437  df-1st 8015  df-2nd 8016  df-neg 11496  df-z 12616  df-uz 12880  df-fz 13549

This theorem is referenced by:  elfzel2  13563  elfzle2  13569  peano2fzr  13578  fzsplit2  13590  fzsplit  13591  fznn0sub  13597  fzopth  13602  fzss1  13604  fzss2  13605  fzp1elp1  13618  predfz  13694  fzosplit  13733  fzoend  13797  fzofzp1b  13805  uzindi  14024  seqcl2  14062  seqfveq2  14066  monoord  14074  sermono  14076  seqsplit  14077  seqf1olem2  14084  seqid2  14090  seqhomo  14091  seqz  14092  bcval5  14358  seqcoll  14504  seqcoll2  14505  swrdval2  14685  pfxres  14718  pfxf  14719  spllen  14793  splfv2a  14795  repswpfx  14824  fsum0diag2  15820  climcndslem2  15887  prodfn0  15931  lcmflefac  16686  pcbc  16939  vdwlem2  17021  vdwlem5  17024  vdwlem6  17025  vdwlem8  17027  prmgaplem1  17088  psgnunilem5  19513  efgsres  19757  efgredleme  19762  efgcpbllemb  19774  imasdsf1olem  24384  volsup  25592  dvn2bss  25967  dvtaylp  26413  wilth  27115  ftalem1  27117  ppisval2  27149  dvdsppwf1o  27230  logfaclbnd  27267  bposlem6  27334  wlkres  29689  fzsplit3  32796  wrdres  32920  pfxf1  32927  swrdrn2  32940  swrdrn3  32941  swrdf1  32942  swrdrndisj  32943  splfv3  32944  pfxchn  33000  cycpmco2f1  33145  cycpmco2rn  33146  cycpmco2lem7  33153  ballotlemsima  34519  ballotlemfrc  34530  ballotlemfrceq  34532  fzssfzo  34555  signstres  34591  fsum2dsub  34623  revpfxsfxrev  35122  swrdrevpfx  35123  pfxwlk  35130  erdszelem7  35203  erdszelem8  35204  poimirlem1  37629  poimirlem2  37630  poimirlem3  37631  poimirlem4  37632  poimirlem7  37635  poimirlem12  37640  poimirlem15  37643  poimirlem16  37644  poimirlem17  37645  poimirlem19  37647  poimirlem20  37648  poimirlem23  37651  poimirlem24  37652  poimirlem25  37653  poimirlem29  37657  poimirlem31  37659  mettrifi  37765  fzsplitnd  41984  aks6d1c2lem4  42129  bcc0  44364  iunincfi  45104  monoordxrv  45497  fmulcl  45601  fmul01lt1lem2  45605  dvnprodlem2  45967  stoweidlem11  46031  stoweidlem17  46037  fourierdlem15  46142  ssfz12  47331  smonoord  47363