ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  elfzle2 Unicode version

Theorem elfzle2 9377
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
StepHypRef Expression
1 elfzuz3 9372 . 2  |-  ( K  e.  ( M ... N )  ->  N  e.  ( ZZ>= `  K )
)
2 eluzle 8966 . 2  |-  ( N  e.  ( ZZ>= `  K
)  ->  K  <_  N )
31, 2syl 14 1  |-  ( K  e.  ( M ... N )  ->  K  <_  N )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1436   class class class wbr 3822   ` cfv 4983  (class class class)co 5615    <_ cle 7470   ZZ>=cuz 8954   ...cfz 9359
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3934  ax-pow 3986  ax-pr 4012  ax-setind 4328  ax-cnex 7383  ax-resscn 7384
This theorem depends on definitions:  df-bi 115  df-3or 923  df-3an 924  df-tru 1290  df-fal 1293  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ne 2252  df-ral 2360  df-rex 2361  df-rab 2364  df-v 2617  df-sbc 2830  df-dif 2990  df-un 2992  df-in 2994  df-ss 3001  df-pw 3417  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3639  df-br 3823  df-opab 3877  df-mpt 3878  df-id 4096  df-xp 4419  df-rel 4420  df-cnv 4421  df-co 4422  df-dm 4423  df-rn 4424  df-res 4425  df-ima 4426  df-iota 4948  df-fun 4985  df-fn 4986  df-f 4987  df-fv 4991  df-ov 5618  df-oprab 5619  df-mpt2 5620  df-neg 7603  df-z 8687  df-uz 8955  df-fz 9360
This theorem is referenced by:  elfz1eq  9384  fzdisj  9401  fznatpl1  9423  fzp1disj  9427  uzdisj  9440  fzneuz  9448  fznuz  9449  elfzmlbm  9473  difelfznle  9477  nn0disj  9480  iseqf1olemqcl  9823  iseqf1olemnab  9825  iseqf1olemab  9826  iseqf1olemqk  9831  iseqf1olemfvp  9834  iseqf1olemqsumkj  9835  iseqf1olemqsumk  9836  iseqf1olemqsum  9837  iseqf1oleml  9840  iseqf1o  9841  bcval4  10060  bcp1nk  10070  zfz1isolemiso  10144  iseqcoll  10147  isummolem3  10664  isummolem2a  10665  fisum  10670  fsumcl2lem  10680  fzm1ndvds  10763  prmind2  11008  prmdvdsfz  11026  hashdvds  11103
  Copyright terms: Public domain W3C validator