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

Theorem leloe 9707
Description: 'Less than or equal to' expressed in terms of 'less than' or 'equals'. (Contributed by NM, 13-May-1999.)
Assertion
Ref Expression
leloe  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <_  B  <->  ( A  <  B  \/  A  =  B )
) )

Proof of Theorem leloe
StepHypRef Expression
1 lenlt 9699 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <_  B  <->  -.  B  <  A ) )
2 eqcom 2459 . . . . 5  |-  ( B  =  A  <->  A  =  B )
32orbi1i 527 . . . 4  |-  ( ( B  =  A  \/  A  <  B )  <->  ( A  =  B  \/  A  <  B ) )
4 orcom 393 . . . 4  |-  ( ( A  =  B  \/  A  <  B )  <->  ( A  <  B  \/  A  =  B ) )
53, 4bitri 257 . . 3  |-  ( ( B  =  A  \/  A  <  B )  <->  ( A  <  B  \/  A  =  B ) )
6 axlttri 9692 . . . . 5  |-  ( ( B  e.  RR  /\  A  e.  RR )  ->  ( B  <  A  <->  -.  ( B  =  A  \/  A  <  B
) ) )
76ancoms 459 . . . 4  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( B  <  A  <->  -.  ( B  =  A  \/  A  <  B
) ) )
87con2bid 335 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( ( B  =  A  \/  A  < 
B )  <->  -.  B  <  A ) )
95, 8syl5rbbr 268 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( -.  B  < 
A  <->  ( A  < 
B  \/  A  =  B ) ) )
101, 9bitrd 261 1  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <_  B  <->  ( A  <  B  \/  A  =  B )
) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    \/ wo 374    /\ wa 375    = wceq 1448    e. wcel 1891   class class class wbr 4374   RRcr 9525    < clt 9662    <_ cle 9663
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-8 1893  ax-9 1900  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432  ax-sep 4497  ax-nul 4506  ax-pow 4554  ax-pr 4612  ax-un 6571  ax-resscn 9583  ax-pre-lttri 9600
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 988  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-eu 2304  df-mo 2305  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-ne 2624  df-nel 2625  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3015  df-sbc 3236  df-csb 3332  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4169  df-br 4375  df-opab 4434  df-mpt 4435  df-id 4727  df-xp 4818  df-rel 4819  df-cnv 4820  df-co 4821  df-dm 4822  df-rn 4823  df-res 4824  df-ima 4825  df-iota 5525  df-fun 5563  df-fn 5564  df-f 5565  df-f1 5566  df-fo 5567  df-f1o 5568  df-fv 5569  df-er 7350  df-en 7557  df-dom 7558  df-sdom 7559  df-pnf 9664  df-mnf 9665  df-xr 9666  df-ltxr 9667  df-le 9668
This theorem is referenced by:  ltle  9709  leltne  9710  lelttr  9711  ltletr  9712  letr  9714  leid  9716  ltlen  9722  leloei  9738  leloed  9765  lemul1  10446  lemul1a  10448  squeeze0  10498  fimaxre  10540  sup3  10555  nn0ge0  10885  nn0sub  10910  elnn0z  10940  xlemul1a  11564  om2uzlti  12158  om2uzlt2i  12159  sqlecan  12375  discr  12403  facdiv  12466  facwordi  12468  resqrex  13325  sqrt2irr  14312  lcmf  14617  efgsfo  17400  efgred  17409  itg2mulc  22717  itgabs  22804  dgrlt  23232  sinq12ge0  23475  sineq0  23488  cxpge0  23640  cxplea  23653  cxple2  23654  cxple2a  23656  cxpcn3lem  23699  cxpcn3  23700  cxpaddlelem  23703  cxpaddle  23704  ang180lem3  23752  atanlogaddlem  23851  rlimcnp2  23904  jensen  23926  amgm  23928  htthlem  26582  hiidge0  26763  staddi  27911  stadd3i  27913  poimirlem28  31970  itgaddnclem2  32003  itgabsnc  32013  pellfund14gap  35737  sineq0ALT  37331  icccncfext  37807  iccpartnel  38843  gboge7  38955  bgoldbtbndlem1  38991  ltnltne  39139  elfzolborelfzop1  40641
  Copyright terms: Public domain W3C validator