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

Theorem lenltd 9541
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 9474 . 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 1756   class class class wbr 4313   RRcr 9302    < clt 9439    <_ cle 9440
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4434  ax-nul 4442  ax-pr 4552
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-rab 2745  df-v 2995  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-sn 3899  df-pr 3901  df-op 3905  df-br 4314  df-opab 4372  df-xp 4867  df-cnv 4869  df-xr 9443  df-le 9445
This theorem is referenced by:  ltnsymd  9544  dedekind  9554  leadd1  9828  leord1  9888  prodge0  10197  lediv1  10215  lemuldiv  10232  lerec  10235  le2msq  10253  lbinfm  10304  suprub  10312  suprleub  10315  supmul1  10316  infmrlb  10332  zsupss  10965  suprzub  10967  rpnnen1lem5  11004  fzdisj  11497  uzdisj  11552  fzouzdisj  11606  fleqceilz  11714  seqf1olem1  11866  seqf1olem2  11867  leexp2  11939  hashf1  12231  seqcoll  12237  seqcoll2  12238  ccatsymb  12302  swrdnd  12347  swrdvalodm2  12354  swrdccatin2  12399  rlimcld2  13077  rlimno1  13152  isercoll  13166  ruclem3  13536  bitsfzolem  13651  bitsmod  13653  sadcaddlem  13674  smupvallem  13700  pcfac  13982  4sqlem11  14037  ramcl2lem  14091  sylow1lem1  16118  recld2  20413  reconnlem2  20426  nmoleub2lem3  20692  ivthlem2  20958  ivthlem3  20959  ovolicopnf  21029  ioombl1lem4  21064  ioorcl2  21074  itg1ge0a  21211  mbfi1fseqlem4  21218  itg2monolem1  21250  itg2cnlem1  21261  dvferm1lem  21478  dvferm2lem  21480  mdegmullem  21571  dgrub  21724  dgrlb  21726  dgreq0  21754  quotcan  21797  aaliou3lem9  21838  radcnvle  21907  abelthlem2  21919  logdivle  22093  cxple  22162  lgsval2lem  22667  pntlem3  22880  padicabv  22901  ssnnssfz  26098  esumpcvgval  26549  eulerpartlems  26765  dstfrvunirn  26879  ballotlemodife  26902  erdszelem7  27107  erdszelem8  27108  supaddc  28443  mblfinlem2  28455  areacirc  28515  rencldnfilem  29185  irrapxlem1  29189  monotoddzzfi  29309  stoweidlem14  29835  stoweidlem52  29873  nn0disj  30765  ssnn0ssfz  30770  suprfinzcl  30774
  Copyright terms: Public domain W3C validator