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

Theorem lenltd 9219
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 9154 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <_  B  <->  -.  B  <  A ) )
41, 2, 3syl2anc 643 1  |-  ( ph  ->  ( A  <_  B  <->  -.  B  <  A ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    e. wcel 1725   class class class wbr 4212   RRcr 8989    < clt 9120    <_ cle 9121
This theorem is referenced by:  ltnsymd  9222  leadd1  9496  leord1  9554  prodge0  9857  lediv1  9875  lemuldiv  9889  lerec  9892  le2msq  9910  lbinfm  9961  suprub  9969  suprleub  9972  supmul1  9973  infmrlb  9989  zsupss  10565  suprzub  10567  rpnnen1lem5  10604  fzdisj  11078  uzdisj  11119  fzouzdisj  11169  seqf1olem1  11362  seqf1olem2  11363  leexp2  11434  hashf1  11706  seqcoll  11712  seqcoll2  11713  rlimcld2  12372  rlimno1  12447  isercoll  12461  ruclem3  12832  bitsfzolem  12946  bitsmod  12948  sadcaddlem  12969  smupvallem  12995  pcfac  13268  4sqlem11  13323  ramcl2lem  13377  sylow1lem1  15232  recld2  18845  reconnlem2  18858  nmoleub2lem3  19123  ivthlem2  19349  ivthlem3  19350  ovolicopnf  19420  ioombl1lem4  19455  ioorcl2  19464  itg1ge0a  19603  mbfi1fseqlem4  19610  itg2monolem1  19642  itg2cnlem1  19653  dvferm1lem  19868  dvferm2lem  19870  mdegmullem  20001  dgrub  20153  dgrlb  20155  dgreq0  20183  quotcan  20226  aaliou3lem9  20267  radcnvle  20336  abelthlem2  20348  logdivle  20517  cxple  20586  lgsval2lem  21090  pntlem3  21303  padicabv  21324  ssnnssfz  24148  esumpcvgval  24468  dstfrvunirn  24732  ballotlemodife  24755  erdszelem7  24883  erdszelem8  24884  dedekind  25187  supaddc  26237  mblfinlem2  26244  areacirc  26297  rencldnfilem  26881  irrapxlem1  26885  monotoddzzfi  27005  stoweidlem14  27739  stoweidlem52  27777  ccatsymb  28179  swrdnd  28182  swrdvalodm2  28188  swrdccatin2  28210  cshwidx  28242  2cshwmod  28257
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-sep 4330  ax-nul 4338  ax-pr 4403
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-br 4213  df-opab 4267  df-xp 4884  df-cnv 4886  df-xr 9124  df-le 9126
  Copyright terms: Public domain W3C validator