Theorem elfzle2 9953

Description: A member of a finite set of sequential integer is less than or equal to the upper bound. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)

Assertion

Ref	Expression
elfzle2	|- ( K e. ( M ... N ) -> K <_ N )

Proof of Theorem elfzle2

Step	Hyp	Ref	Expression
1		elfzuz3 9948	. 2 |- ( K e. ( M ... N ) -> N e. ( ZZ>= ` K ) )
2		eluzle 9469	. 2 |- ( N e. ( ZZ>= ` K ) -> K <_ N )
3	1, 2	syl 14	1 |- ( K e. ( M ... N ) -> K <_ N )

Syntax hints:   -> wi 4   e. wcel 2135   class class class wbr 3976   ` cfv 5182  (class class class)co 5836   <_ cle 7925   ZZ>=cuz 9457   ...cfz 9935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-14 2138  ax-ext 2146  ax-sep 4094  ax-pow 4147  ax-pr 4181  ax-setind 4508  ax-cnex 7835  ax-resscn 7836

This theorem depends on definitions:  df-bi 116  df-3or 968  df-3an 969  df-tru 1345  df-fal 1348  df-nf 1448  df-sb 1750  df-eu 2016  df-mo 2017  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-ne 2335  df-ral 2447  df-rex 2448  df-rab 2451  df-v 2723  df-sbc 2947  df-dif 3113  df-un 3115  df-in 3117  df-ss 3124  df-pw 3555  df-sn 3576  df-pr 3577  df-op 3579  df-uni 3784  df-br 3977  df-opab 4038  df-mpt 4039  df-id 4265  df-xp 4604  df-rel 4605  df-cnv 4606  df-co 4607  df-dm 4608  df-rn 4609  df-res 4610  df-ima 4611  df-iota 5147  df-fun 5184  df-fn 5185  df-f 5186  df-fv 5190  df-ov 5839  df-oprab 5840  df-mpo 5841  df-neg 8063  df-z 9183  df-uz 9458  df-fz 9936

This theorem is referenced by:  elfz1eq  9960  fzdisj  9977  fznatpl1  10001  fzp1disj  10005  uzdisj  10018  fzneuz  10026  fznuz  10027  elfzmlbm  10056  difelfznle  10060  nn0disj  10063  iseqf1olemqcl  10411  iseqf1olemnab  10413  iseqf1olemab  10414  iseqf1olemqk  10419  iseqf1olemfvp  10422  seq3f1olemqsumkj  10423  seq3f1olemqsumk  10424  seq3f1olemqsum  10425  seq3f1oleml  10428  seq3f1o  10429  bcval4  10654  bcp1nk  10664  zfz1isolemiso  10738  seq3coll  10741  summodclem3  11307  summodclem2a  11308  fsum3  11314  fsumcl2lem  11325  fsum0diaglem  11367  mertenslemi1  11462  prodmodclem3  11502  prodmodclem2a  11503  fprodseq  11510  fzm1ndvds  11779  prmind2  12031  prmdvdsfz  12050  hashdvds  12130  eulerthlemrprm  12138  eulerthlema  12139  prmdiveq  12145  ennnfonelemim  12294  ctinfomlemom  12297  supfz  13781