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

Theorem lenltd 9781
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 9712 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <_  B  <->  -.  B  <  A ) )
41, 2, 3syl2anc 667 1  |-  ( ph  ->  ( A  <_  B  <->  -.  B  <  A ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 188    e. wcel 1887   class class class wbr 4402   RRcr 9538    < clt 9675    <_ cle 9676
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pr 4639
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-br 4403  df-opab 4462  df-xp 4840  df-cnv 4842  df-xr 9679  df-le 9681
This theorem is referenced by:  ltnsymd  9784  nltled  9785  lensymd  9786  dedekind  9797  leadd1  10082  leord1  10141  prodge0  10452  lediv1  10470  lemuldiv  10486  lerec  10489  le2msq  10506  lbinfmOLD  10560  suprub  10570  suprleub  10573  supaddc  10574  supmul1  10576  infregelb  10594  infmrlbOLD  10597  suprfinzcl  11050  uzinfi  11238  zsupss  11253  suprzub  11255  rpnnen1lem5  11294  fzdisj  11826  uzdisj  11867  nn0disj  11907  fzouzdisj  11954  fleqceilz  12081  seqf1olem1  12252  seqf1olem2  12253  leexp2  12327  hashf1  12620  seqcoll  12627  seqcoll2  12628  ccatsymb  12727  swrdccatin2  12843  rlimcld2  13642  rlimno1  13717  isercoll  13731  ruclem3  14285  bitsfzolem  14407  bitsfzolemOLD  14408  bitsmod  14410  sadcaddlem  14431  smupvallem  14457  pcfac  14844  4sqlem11  14899  ramcl2lem  14962  ramcl2lemOLD  14963  sylow1lem1  17250  fvmptnn04if  19873  chfacfisf  19878  chfacfisfcpmat  19879  recld2  21832  reconnlem2  21845  nmoleub2lem3  22129  ivthlem2  22403  ivthlem3  22404  ovolicopnf  22478  ioombl1lem4  22514  ioorcl2  22524  itg1ge0a  22669  mbfi1fseqlem4  22676  itg2monolem1  22708  itg2cnlem1  22719  dvferm1lem  22936  dvferm2lem  22938  mdegmullem  23027  dgrub  23188  dgrlb  23190  dgreq0  23219  quotcan  23262  aaliou3lem9  23306  radcnvle  23375  abelthlem2  23387  logdivle  23571  cxple  23640  lgsval2lem  24234  padicabv  24468  ssnnssfz  28367  smattr  28625  smatbl  28626  smatbr  28627  esumpcvgval  28899  eulerpartlems  29193  dstfrvunirn  29307  ballotlemodife  29330  erdszelem7  29920  erdszelem8  29921  poimirlem2  31942  poimirlem7  31947  poimirlem10  31950  poimirlem11  31951  mblfinlem2  31978  areacirc  32037  rencldnfilem  35663  irrapxlem1  35666  monotoddzzfi  35790  radcnvrat  36663  dvnxpaek  37817  fourierdlem12  37981  fourierdlem42  38012  fourierdlem42OLD  38013  elaa2lem  38097  elaa2lemOLD  38098  iundjiun  38298  volico  38363  hoidmvval0  38409  hoidmv1lelem2  38414  hoidmv1lelem3  38415  hoidmvlelem4  38420  hspdifhsp  38438  fzopredsuc  38720  stgoldbwt  38877  nnsum3primesle9  38889  bgoldbtbndlem1  38900  ssnn0ssfz  40183
  Copyright terms: Public domain W3C validator