Theorem elfzuz3 13482

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

Syntax hints:   → wi 4   ∈ wcel 2109  ‘cfv 6511  (class class class)co 7387  ℤ_≥cuz 12793  ...cfz 13468

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 5251  ax-nul 5261  ax-pr 5387  ax-un 7711  ax-cnex 11124  ax-resscn 11125

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 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fv 6519  df-ov 7390  df-oprab 7391  df-mpo 7392  df-1st 7968  df-2nd 7969  df-neg 11408  df-z 12530  df-uz 12794  df-fz 13469

This theorem is referenced by:  elfzel2  13483  elfzle2  13489  peano2fzr  13498  fzsplit2  13510  fzsplit  13511  fznn0sub  13517  fzopth  13522  fzss1  13524  fzss2  13525  fzp1elp1  13538  predfz  13614  fzosplit  13653  fzoend  13718  fzofzp1b  13726  uzindi  13947  seqcl2  13985  seqfveq2  13989  monoord  13997  sermono  13999  seqsplit  14000  seqf1olem2  14007  seqid2  14013  seqhomo  14014  seqz  14015  bcval5  14283  seqcoll  14429  seqcoll2  14430  swrdval2  14611  pfxres  14644  pfxf  14645  spllen  14719  splfv2a  14721  repswpfx  14750  fsum0diag2  15749  climcndslem2  15816  prodfn0  15860  lcmflefac  16618  pcbc  16871  vdwlem2  16953  vdwlem5  16956  vdwlem6  16957  vdwlem8  16959  prmgaplem1  17020  psgnunilem5  19424  efgsres  19668  efgredleme  19673  efgcpbllemb  19685  imasdsf1olem  24261  volsup  25457  dvn2bss  25832  dvtaylp  26278  wilth  26981  ftalem1  26983  ppisval2  27015  dvdsppwf1o  27096  logfaclbnd  27133  bposlem6  27200  wlkres  29598  fzsplit3  32716  wrdres  32856  pfxf1  32863  swrdrn2  32876  swrdrn3  32877  swrdf1  32878  swrdrndisj  32879  splfv3  32880  pfxchn  32935  cycpmco2f1  33081  cycpmco2rn  33082  cycpmco2lem7  33089  ballotlemsima  34507  ballotlemfrc  34518  ballotlemfrceq  34520  fzssfzo  34530  signstres  34566  fsum2dsub  34598  revpfxsfxrev  35103  swrdrevpfx  35104  pfxwlk  35111  erdszelem7  35184  erdszelem8  35185  poimirlem1  37615  poimirlem2  37616  poimirlem3  37617  poimirlem4  37618  poimirlem7  37621  poimirlem12  37626  poimirlem15  37629  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem23  37637  poimirlem24  37638  poimirlem25  37639  poimirlem29  37643  poimirlem31  37645  mettrifi  37751  fzsplitnd  41970  aks6d1c2lem4  42115  bcc0  44329  iunincfi  45088  monoordxrv  45477  fmulcl  45579  fmul01lt1lem2  45583  dvnprodlem2  45945  stoweidlem11  46009  stoweidlem17  46015  fourierdlem15  46120  ssfz12  47315  smonoord  47372