Theorem elfzuz3 13503

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

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

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 7728  ax-cnex 11169  ax-resscn 11170

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 7978  df-2nd 7979  df-neg 11452  df-z 12564  df-uz 12828  df-fz 13490

This theorem is referenced by:  elfzel2  13504  elfzle2  13510  peano2fzr  13519  fzsplit2  13531  fzsplit  13532  fznn0sub  13538  fzopth  13543  fzss1  13545  fzss2  13546  fzp1elp1  13559  predfz  13631  fzosplit  13670  fzoend  13728  fzofzp1b  13735  uzindi  13952  seqcl2  13991  seqfveq2  13995  monoord  14003  sermono  14005  seqsplit  14006  seqf1olem2  14013  seqid2  14019  seqhomo  14020  seqz  14021  bcval5  14283  seqcoll  14430  seqcoll2  14431  swrdval2  14601  pfxres  14634  pfxf  14635  spllen  14709  splfv2a  14711  repswpfx  14740  fsum0diag2  15734  climcndslem2  15801  prodfn0  15845  lcmflefac  16590  pcbc  16838  vdwlem2  16920  vdwlem5  16923  vdwlem6  16924  vdwlem8  16926  prmgaplem1  16987  psgnunilem5  19404  efgsres  19648  efgredleme  19653  efgcpbllemb  19665  imasdsf1olem  24100  volsup  25306  dvn2bss  25681  dvtaylp  26119  wilth  26812  ftalem1  26814  ppisval2  26846  dvdsppwf1o  26927  logfaclbnd  26962  bposlem6  27029  wlkres  29195  fzsplit3  32273  wrdres  32371  pfxf1  32376  swrdrn2  32386  swrdrn3  32387  swrdf1  32388  swrdrndisj  32389  splfv3  32390  cycpmco2f1  32554  cycpmco2rn  32555  cycpmco2lem7  32562  ballotlemsima  33813  ballotlemfrc  33824  ballotlemfrceq  33826  fzssfzo  33849  signstres  33885  fsum2dsub  33918  revpfxsfxrev  34405  swrdrevpfx  34406  pfxwlk  34413  erdszelem7  34487  erdszelem8  34488  poimirlem1  36793  poimirlem2  36794  poimirlem3  36795  poimirlem4  36796  poimirlem7  36799  poimirlem12  36804  poimirlem15  36807  poimirlem16  36808  poimirlem17  36809  poimirlem19  36811  poimirlem20  36812  poimirlem23  36815  poimirlem24  36816  poimirlem25  36817  poimirlem29  36821  poimirlem31  36823  mettrifi  36929  fzsplitnd  41155  bcc0  43402  iunincfi  44085  monoordxrv  44491  fmulcl  44596  fmul01lt1lem2  44600  dvnprodlem2  44962  stoweidlem11  45026  stoweidlem17  45032  fourierdlem15  45137  ssfz12  46321  smonoord  46338