Theorem elfzuz 10020

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 10018	. 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 2148   ` cfv 5216  (class class class)co 5874   ZZ>=cuz 9527   ...cfz 10007

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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4121  ax-pow 4174  ax-pr 4209  ax-setind 4536  ax-cnex 7901  ax-resscn 7902

This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2739  df-sbc 2963  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-br 4004  df-opab 4065  df-mpt 4066  df-id 4293  df-xp 4632  df-rel 4633  df-cnv 4634  df-co 4635  df-dm 4636  df-rn 4637  df-res 4638  df-ima 4639  df-iota 5178  df-fun 5218  df-fn 5219  df-f 5220  df-fv 5224  df-ov 5877  df-oprab 5878  df-mpo 5879  df-neg 8130  df-z 9253  df-uz 9528  df-fz 10008

This theorem is referenced by:  elfzel1  10023  elfzelz  10024  elfzle1  10026  eluzfz2b  10032  fzsplit2  10049  fzsplit  10050  fzopth  10060  fzss1  10062  fzss2  10063  fzssuz  10064  fzp1elp1  10074  uzsplit  10091  elfzmlbm  10130  fzosplit  10176  seq3feq2  10469  seq3feq  10471  ser3mono  10477  seq3caopr3  10480  iseqf1olemkle  10483  iseqf1olemklt  10484  iseqf1olemnab  10487  iseqf1olemqk  10493  iseqf1olemjpcl  10494  iseqf1olemqpcl  10495  iseqf1olemfvp  10496  seq3f1olemqsumkj  10497  seq3f1olemqsumk  10498  seq3f1olemqsum  10499  seq3f1olemstep  10500  seq3f1oleml  10502  seq3f1o  10503  seq3z  10510  ser0  10513  ser3le  10517  seq3coll  10821  climub  11351  sumrbdclem  11384  fsum3cvg  11385  fsum3ser  11404  fsump1i  11440  fsum0diaglem  11447  iserabs  11482  isumsplit  11498  isum1p  11499  geosergap  11513  mertenslemi1  11542  prodf1  11549  prodfap0  11552  prodfrecap  11553  prodfdivap  11554  prodrbdclem  11578  fproddccvg  11579  fprodntrivap  11591  fprodabs  11623  fprodeq0  11624  infssuzex  11949  prmind2  12119  prmdvdsfz  12138  isprm5lem  12140  eulerthlemrprm  12228  eulerthlema  12229  pcfac  12347  lgsdilem2  14407  cvgcmp2nlemabs  14750