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

Theorem lenltd 9734
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 9666 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <_  B  <->  -.  B  <  A ) )
41, 2, 3syl2anc 661 1  |-  ( ph  ->  ( A  <_  B  <->  -.  B  <  A ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    e. wcel 1804   class class class wbr 4437   RRcr 9494    < clt 9631    <_ cle 9632
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-br 4438  df-opab 4496  df-xp 4995  df-cnv 4997  df-xr 9635  df-le 9637
This theorem is referenced by:  ltnsymd  9737  dedekind  9747  leadd1  10027  leord1  10087  prodge0  10396  lediv1  10414  lemuldiv  10431  lerec  10434  le2msq  10452  lbinfm  10503  suprub  10511  suprleub  10514  supmul1  10515  infmrlb  10531  suprfinzcl  10985  zsupss  11182  suprzub  11184  rpnnen1lem5  11223  fzdisj  11723  uzdisj  11762  nn0disj  11802  fzouzdisj  11843  fleqceilz  11963  seqf1olem1  12128  seqf1olem2  12129  leexp2  12202  hashf1  12488  seqcoll  12494  seqcoll2  12495  ccatsymb  12582  swrdnd  12639  swrdvalodm2  12646  swrdccatin2  12694  rlimcld2  13383  rlimno1  13458  isercoll  13472  ruclem3  13948  bitsfzolem  14066  bitsmod  14068  sadcaddlem  14089  smupvallem  14115  pcfac  14400  4sqlem11  14455  ramcl2lem  14509  sylow1lem1  16597  fvmptnn04if  19328  chfacfisf  19333  chfacfisfcpmat  19334  recld2  21297  reconnlem2  21310  nmoleub2lem3  21576  ivthlem2  21842  ivthlem3  21843  ovolicopnf  21913  ioombl1lem4  21949  ioorcl2  21959  itg1ge0a  22096  mbfi1fseqlem4  22103  itg2monolem1  22135  itg2cnlem1  22146  dvferm1lem  22363  dvferm2lem  22365  mdegmullem  22456  dgrub  22609  dgrlb  22611  dgreq0  22640  quotcan  22683  aaliou3lem9  22724  radcnvle  22793  abelthlem2  22805  logdivle  22985  cxple  23054  lgsval2lem  23559  pntlem3  23772  padicabv  23793  ssnnssfz  27575  esumpcvgval  28062  eulerpartlems  28277  dstfrvunirn  28391  ballotlemodife  28414  erdszelem7  28619  erdszelem8  28620  supaddc  30017  mblfinlem2  30028  areacirc  30088  rencldnfilem  30730  irrapxlem1  30734  monotoddzzfi  30854  radcnvrat  31171  lcmgcdlem  31188  lensymd  31424  nltled  31431  dvnxpaek  31693  fourierdlem12  31855  fourierdlem42  31885  elaa2lem  31970  etransclem3  31974  etransclem7  31978  etransclem10  31981  etransclem15  31986  etransclem20  31991  etransclem21  31992  etransclem22  31993  etransclem24  31995  etransclem25  31996  etransclem27  31998  etransclem32  32003  etransclem35  32006  etransc  32020  ssnn0ssfz  32806
  Copyright terms: Public domain W3C validator