Theorem elfzuz3 13578

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ‘cfv 6533  (class class class)co 7414  ℤ_≥cuz 12890  ...cfz 13564

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-un 7737  ax-cnex 11183  ax-resscn 11184

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  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 6489  df-fun 6535  df-fn 6536  df-f 6537  df-fv 6541  df-ov 7417  df-oprab 7418  df-mpo 7419  df-1st 7987  df-2nd 7988  df-neg 11471  df-z 12619  df-uz 12891  df-fz 13565

This theorem is used by:  elfzel2  13579  elfzle2  13585  peano2fzr  13594  fzsplit2  13607  fzsplit  13608  fznn0sub  13614  fzopth  13619  fzss1  13621  fzss2  13622  fzp1elp1  13635  predfz  13711  fzosplit  13751  fzoend  13816  fzofzp1b  13824  uzindi  14049  seqcl2  14087  seqfveq2  14091  monoord  14099  sermono  14101  seqsplit  14102  seqf1olem2  14109  seqid2  14115  seqhomo  14116  seqz  14117  bcval5  14385  seqcoll  14532  seqcoll2  14533  swrdval2  14717  swrdf1  14722  swrdrn3  14725  pfxres  14752  pfxf  14753  spllen  14826  splfv2a  14828  revpfxsfxrev  14840  swrdrevpfx  14841  repswpfx  14859  fsum0diag2  15872  climcndslem2  15942  prodfn0  15986  lcmflefac  16741  pcbc  16995  vdwlem2  17077  vdwlem5  17080  vdwlem6  17081  vdwlem8  17083  prmgaplem1  17144  pfxchn  18701  psgnunilem5  19624  efgsres  19868  efgredleme  19873  efgcpbllemb  19885  imasdsf1olem  24602  volsup  25787  dvn2bss  26160  dvtaylp  26609  wilth  27310  ftalem1  27312  ppisval2  27344  dvdsppwf1o  27425  logfaclbnd  27461  bposlem6  27528  wlkres  30131  pfxwlk  30148  fzsplit3  33267  wrdres  33384  pfxf1  33391  swrdrn2  33399  swrdrndisj  33400  splfv3  33401  cycpmco2f1  33567  cycpmco2rn  33568  cycpmco2lem7  33575  ballotlemsima  35030  ballotlemfrc  35041  ballotlemfrceq  35043  fzssfzo  35053  signstres  35086  fsum2dsub  35118  erdszelem7  35779  erdszelem8  35780  poimirlem1  38373  poimirlem2  38374  poimirlem3  38375  poimirlem4  38376  poimirlem7  38379  poimirlem12  38384  poimirlem15  38387  poimirlem16  38388  poimirlem17  38389  poimirlem19  38391  poimirlem20  38392  poimirlem23  38395  poimirlem24  38396  poimirlem25  38397  poimirlem29  38401  poimirlem31  38403  mettrifi  38510  fzsplitnd  42851  aks6d1c2lem4  42996  bcc0  45167  iunincfi  45929  monoordxrv  46312  fmulcl  46414  fmul01lt1lem2  46418  dvnprodlem2  46778  stoweidlem11  46842  stoweidlem17  46848  fourierdlem15  46953  ssfz12  48205  smonoord  48268