Theorem elfzuz 10185

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 10183	. 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 2180   ` cfv 5294  (class class class)co 5974   ZZ>=cuz 9690   ...cfz 10172

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 617  ax-in2 618  ax-io 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-14 2183  ax-ext 2191  ax-sep 4181  ax-pow 4237  ax-pr 4272  ax-setind 4606  ax-cnex 8058  ax-resscn 8059

This theorem depends on definitions:  df-bi 117  df-3or 984  df-3an 985  df-tru 1378  df-fal 1381  df-nf 1487  df-sb 1789  df-eu 2060  df-mo 2061  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-ne 2381  df-ral 2493  df-rex 2494  df-rab 2497  df-v 2781  df-sbc 3009  df-dif 3179  df-un 3181  df-in 3183  df-ss 3190  df-pw 3631  df-sn 3652  df-pr 3653  df-op 3655  df-uni 3868  df-br 4063  df-opab 4125  df-mpt 4126  df-id 4361  df-xp 4702  df-rel 4703  df-cnv 4704  df-co 4705  df-dm 4706  df-rn 4707  df-res 4708  df-ima 4709  df-iota 5254  df-fun 5296  df-fn 5297  df-f 5298  df-fv 5302  df-ov 5977  df-oprab 5978  df-mpo 5979  df-neg 8288  df-z 9415  df-uz 9691  df-fz 10173

This theorem is referenced by:  elfzel1  10188  elfzelz  10189  elfzle1  10191  eluzfz2b  10197  fzsplit2  10214  fzsplit  10215  fzopth  10225  fzss1  10227  fzss2  10228  fzssuz  10229  fzp1elp1  10239  uzsplit  10256  elfzmlbm  10295  fzosplit  10343  infssuzex  10420  seq3feq2  10665  seq3feq  10669  ser3mono  10676  seq3caopr3  10680  iseqf1olemkle  10686  iseqf1olemklt  10687  iseqf1olemnab  10690  iseqf1olemqk  10696  iseqf1olemjpcl  10697  iseqf1olemqpcl  10698  iseqf1olemfvp  10699  seq3f1olemqsumkj  10700  seq3f1olemqsumk  10701  seq3f1olemqsum  10702  seq3f1olemstep  10703  seq3f1oleml  10705  seq3f1o  10706  seqf1oglem2  10709  seq3z  10717  ser0  10722  ser3le  10726  seq3coll  11031  swrdval2  11149  swrdswrd  11203  pfxccatin12  11231  pfxccatpfx2  11235  climub  11821  sumrbdclem  11854  fsum3cvg  11855  fsum3ser  11874  fsump1i  11910  fsum0diaglem  11917  iserabs  11952  isumsplit  11968  isum1p  11969  geosergap  11983  mertenslemi1  12012  prodf1  12019  prodfap0  12022  prodfrecap  12023  prodfdivap  12024  prodrbdclem  12048  fproddccvg  12049  fprodntrivap  12061  fprodabs  12093  fprodeq0  12094  nninfctlemfo  12527  prmind2  12608  prmdvdsfz  12627  isprm5lem  12629  eulerthlemrprm  12717  eulerthlema  12718  pcfac  12839  mersenne  15636  lgsdilem2  15680  cvgcmp2nlemabs  16311