Theorem elfzuz3 13505

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

Syntax hints:   → wi 4   ∈ wcel 2105  ‘cfv 6543  (class class class)co 7412  ℤ_≥cuz 12829  ...cfz 13491

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7729  ax-cnex 11172  ax-resscn 11173

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-ov 7415  df-oprab 7416  df-mpo 7417  df-1st 7979  df-2nd 7980  df-neg 11454  df-z 12566  df-uz 12830  df-fz 13492

This theorem is referenced by:  elfzel2  13506  elfzle2  13512  peano2fzr  13521  fzsplit2  13533  fzsplit  13534  fznn0sub  13540  fzopth  13545  fzss1  13547  fzss2  13548  fzp1elp1  13561  predfz  13633  fzosplit  13672  fzoend  13730  fzofzp1b  13737  uzindi  13954  seqcl2  13993  seqfveq2  13997  monoord  14005  sermono  14007  seqsplit  14008  seqf1olem2  14015  seqid2  14021  seqhomo  14022  seqz  14023  bcval5  14285  seqcoll  14432  seqcoll2  14433  swrdval2  14603  pfxres  14636  pfxf  14637  spllen  14711  splfv2a  14713  repswpfx  14742  fsum0diag2  15736  climcndslem2  15803  prodfn0  15847  lcmflefac  16592  pcbc  16840  vdwlem2  16922  vdwlem5  16925  vdwlem6  16926  vdwlem8  16928  prmgaplem1  16989  psgnunilem5  19410  efgsres  19654  efgredleme  19659  efgcpbllemb  19671  imasdsf1olem  24199  volsup  25405  dvn2bss  25780  dvtaylp  26221  wilth  26917  ftalem1  26919  ppisval2  26951  dvdsppwf1o  27032  logfaclbnd  27069  bposlem6  27136  wlkres  29361  fzsplit3  32439  wrdres  32537  pfxf1  32542  swrdrn2  32552  swrdrn3  32553  swrdf1  32554  swrdrndisj  32555  splfv3  32556  cycpmco2f1  32720  cycpmco2rn  32721  cycpmco2lem7  32728  ballotlemsima  33979  ballotlemfrc  33990  ballotlemfrceq  33992  fzssfzo  34015  signstres  34051  fsum2dsub  34084  revpfxsfxrev  34571  swrdrevpfx  34572  pfxwlk  34579  erdszelem7  34653  erdszelem8  34654  poimirlem1  36955  poimirlem2  36956  poimirlem3  36957  poimirlem4  36958  poimirlem7  36961  poimirlem12  36966  poimirlem15  36969  poimirlem16  36970  poimirlem17  36971  poimirlem19  36973  poimirlem20  36974  poimirlem23  36977  poimirlem24  36978  poimirlem25  36979  poimirlem29  36983  poimirlem31  36985  mettrifi  37091  fzsplitnd  41317  bcc0  43564  iunincfi  44247  monoordxrv  44653  fmulcl  44758  fmul01lt1lem2  44762  dvnprodlem2  45124  stoweidlem11  45188  stoweidlem17  45194  fourierdlem15  45299  ssfz12  46483  smonoord  46500