Theorem elfzuz 10261

Description: A member of a finite set of sequential integers belongs to an upper set of integers. (Contributed by NM, 17-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)

Assertion

Ref	Expression
elfzuz	|- ( K e. ( M ... N ) -> K e. ( ZZ>= ` M ) )

Proof of Theorem elfzuz

Step	Hyp	Ref	Expression
1		elfzuzb 10259	. 2 |- ( K e. ( M ... N ) <-> ( K e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) )
2	1	simplbi 274	1 |- ( K e. ( M ... N ) -> K e. ( ZZ>= ` M ) )

Syntax hints:   -> wi 4   e. wcel 2201   ` cfv 5328  (class class class)co 6023   ZZ>=cuz 9760   ...cfz 10248

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2204  ax-ext 2212  ax-sep 4208  ax-pow 4266  ax-pr 4301  ax-setind 4637  ax-cnex 8128  ax-resscn 8129

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1810  df-eu 2081  df-mo 2082  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-ne 2402  df-ral 2514  df-rex 2515  df-rab 2518  df-v 2803  df-sbc 3031  df-dif 3201  df-un 3203  df-in 3205  df-ss 3212  df-pw 3655  df-sn 3676  df-pr 3677  df-op 3679  df-uni 3895  df-br 4090  df-opab 4152  df-mpt 4153  df-id 4392  df-xp 4733  df-rel 4734  df-cnv 4735  df-co 4736  df-dm 4737  df-rn 4738  df-res 4739  df-ima 4740  df-iota 5288  df-fun 5330  df-fn 5331  df-f 5332  df-fv 5336  df-ov 6026  df-oprab 6027  df-mpo 6028  df-neg 8358  df-z 9485  df-uz 9761  df-fz 10249

This theorem is referenced by:  elfzel1  10264  elfzelz  10265  elfzle1  10267  eluzfz2b  10273  fzsplit2  10290  fzsplit  10291  fzopth  10301  fzss1  10303  fzss2  10304  fzssuz  10305  fzp1elp1  10315  uzsplit  10332  elfzmlbm  10371  fzosplit  10419  infssuzex  10499  seq3feq2  10744  seq3feq  10748  ser3mono  10755  seq3caopr3  10759  iseqf1olemkle  10765  iseqf1olemklt  10766  iseqf1olemnab  10769  iseqf1olemqk  10775  iseqf1olemjpcl  10776  iseqf1olemqpcl  10777  iseqf1olemfvp  10778  seq3f1olemqsumkj  10779  seq3f1olemqsumk  10780  seq3f1olemqsum  10781  seq3f1olemstep  10782  seq3f1oleml  10784  seq3f1o  10785  seqf1oglem2  10788  seq3z  10796  ser0  10801  ser3le  10805  seq3coll  11112  swrdval2  11241  swrdswrd  11295  pfxccatin12  11323  pfxccatpfx2  11327  climub  11927  sumrbdclem  11961  fsum3cvg  11962  fsum3ser  11981  fsump1i  12017  fsum0diaglem  12024  iserabs  12059  isumsplit  12075  isum1p  12076  geosergap  12090  mertenslemi1  12119  prodf1  12126  prodfap0  12129  prodfrecap  12130  prodfdivap  12131  prodrbdclem  12155  fproddccvg  12156  fprodntrivap  12168  fprodabs  12200  fprodeq0  12201  nninfctlemfo  12634  prmind2  12715  prmdvdsfz  12734  isprm5lem  12736  eulerthlemrprm  12824  eulerthlema  12825  pcfac  12946  mersenne  15750  lgsdilem2  15794  cvgcmp2nlemabs  16703