MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lenltd Structured version   Unicode version

Theorem lenltd 9782
Description: 'Less than or equal to' in terms of 'less than'. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
ltd.1  |-  ( ph  ->  A  e.  RR )
ltd.2  |-  ( ph  ->  B  e.  RR )
Assertion
Ref Expression
lenltd  |-  ( ph  ->  ( A  <_  B  <->  -.  B  <  A ) )

Proof of Theorem lenltd
StepHypRef Expression
1 ltd.1 . 2  |-  ( ph  ->  A  e.  RR )
2 ltd.2 . 2  |-  ( ph  ->  B  e.  RR )
3 lenlt 9713 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <_  B  <->  -.  B  <  A ) )
41, 2, 3syl2anc 665 1  |-  ( ph  ->  ( A  <_  B  <->  -.  B  <  A ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    e. wcel 1868   class class class wbr 4420   RRcr 9539    < clt 9676    <_ cle 9677
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pr 4657
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-br 4421  df-opab 4480  df-xp 4856  df-cnv 4858  df-xr 9680  df-le 9682
This theorem is referenced by:  ltnsymd  9785  nltled  9786  lensymd  9787  dedekind  9798  leadd1  10083  leord1  10142  prodge0  10453  lediv1  10471  lemuldiv  10487  lerec  10490  le2msq  10507  lbinfmOLD  10561  suprub  10571  suprleub  10574  supaddc  10575  supmul1  10577  infregelb  10595  infmrlbOLD  10598  suprfinzcl  11051  uzinfi  11239  zsupss  11254  suprzub  11256  rpnnen1lem5  11295  fzdisj  11827  uzdisj  11868  nn0disj  11908  fzouzdisj  11955  fleqceilz  12081  seqf1olem1  12252  seqf1olem2  12253  leexp2  12327  hashf1  12618  seqcoll  12625  seqcoll2  12626  ccatsymb  12720  swrdccatin2  12834  rlimcld2  13630  rlimno1  13705  isercoll  13719  ruclem3  14273  bitsfzolem  14395  bitsfzolemOLD  14396  bitsmod  14398  sadcaddlem  14419  smupvallem  14445  pcfac  14832  4sqlem11  14887  ramcl2lem  14950  ramcl2lemOLD  14951  sylow1lem1  17238  fvmptnn04if  19860  chfacfisf  19865  chfacfisfcpmat  19866  recld2  21819  reconnlem2  21832  nmoleub2lem3  22116  ivthlem2  22390  ivthlem3  22391  ovolicopnf  22465  ioombl1lem4  22501  ioorcl2  22511  itg1ge0a  22656  mbfi1fseqlem4  22663  itg2monolem1  22695  itg2cnlem1  22706  dvferm1lem  22923  dvferm2lem  22925  mdegmullem  23014  dgrub  23175  dgrlb  23177  dgreq0  23206  quotcan  23249  aaliou3lem9  23293  radcnvle  23362  abelthlem2  23374  logdivle  23558  cxple  23627  lgsval2lem  24221  padicabv  24455  ssnnssfz  28361  smattr  28621  smatbl  28622  smatbr  28623  esumpcvgval  28895  eulerpartlems  29189  dstfrvunirn  29303  ballotlemodife  29326  erdszelem7  29916  erdszelem8  29917  poimirlem2  31856  poimirlem7  31861  poimirlem10  31864  poimirlem11  31865  mblfinlem2  31892  areacirc  31951  rencldnfilem  35582  irrapxlem1  35586  monotoddzzfi  35710  radcnvrat  36521  dvnxpaek  37637  fourierdlem12  37801  fourierdlem42  37832  fourierdlem42OLD  37833  elaa2lem  37917  elaa2lemOLD  37918  iundjiun  38077  volico  38138  fzopredsuc  38432  stgoldbwt  38589  nnsum3primesle9  38601  bgoldbtbndlem1  38612  ssnn0ssfz  39404
  Copyright terms: Public domain W3C validator