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

Theorem lenltd 9507
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 9440 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <_  B  <->  -.  B  <  A ) )
41, 2, 3syl2anc 654 1  |-  ( ph  ->  ( A  <_  B  <->  -.  B  <  A ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    e. wcel 1755   class class class wbr 4280   RRcr 9268    < clt 9405    <_ cle 9406
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-br 4281  df-opab 4339  df-xp 4833  df-cnv 4835  df-xr 9409  df-le 9411
This theorem is referenced by:  ltnsymd  9510  dedekind  9520  leadd1  9794  leord1  9854  prodge0  10163  lediv1  10181  lemuldiv  10198  lerec  10201  le2msq  10219  lbinfm  10270  suprub  10278  suprleub  10281  supmul1  10282  infmrlb  10298  zsupss  10931  suprzub  10933  rpnnen1lem5  10970  fzdisj  11462  uzdisj  11514  fzouzdisj  11568  fleqceilz  11676  seqf1olem1  11828  seqf1olem2  11829  leexp2  11901  hashf1  12193  seqcoll  12199  seqcoll2  12200  ccatsymb  12264  swrdnd  12309  swrdvalodm2  12316  swrdccatin2  12361  rlimcld2  13039  rlimno1  13114  isercoll  13128  ruclem3  13497  bitsfzolem  13612  bitsmod  13614  sadcaddlem  13635  smupvallem  13661  pcfac  13943  4sqlem11  13998  ramcl2lem  14052  sylow1lem1  16076  recld2  20232  reconnlem2  20245  nmoleub2lem3  20511  ivthlem2  20777  ivthlem3  20778  ovolicopnf  20848  ioombl1lem4  20883  ioorcl2  20893  itg1ge0a  21030  mbfi1fseqlem4  21037  itg2monolem1  21069  itg2cnlem1  21080  dvferm1lem  21297  dvferm2lem  21299  mdegmullem  21433  dgrub  21586  dgrlb  21588  dgreq0  21616  quotcan  21659  aaliou3lem9  21700  radcnvle  21769  abelthlem2  21781  logdivle  21955  cxple  22024  lgsval2lem  22529  pntlem3  22742  padicabv  22763  ssnnssfz  25898  esumpcvgval  26380  eulerpartlems  26590  dstfrvunirn  26704  ballotlemodife  26727  erdszelem7  26932  erdszelem8  26933  supaddc  28258  mblfinlem2  28270  areacirc  28330  rencldnfilem  29001  irrapxlem1  29005  monotoddzzfi  29125  stoweidlem14  29652  stoweidlem52  29690
  Copyright terms: Public domain W3C validator