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

Theorem lenlt 10707
Description: 'Less than or equal to' expressed in terms of 'less than'. (Contributed by NM, 13-May-1999.)
Assertion
Ref Expression
lenlt ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))

Proof of Theorem lenlt
StepHypRef Expression
1 rexr 10675 . 2 (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
2 rexr 10675 . 2 (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*)
3 xrlenlt 10694 . 2 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))
41, 2, 3syl2an 595 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wcel 2105   class class class wbr 5057  cr 10524  *cxr 10662   < clt 10663  cle 10664
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-br 5058  df-opab 5120  df-xp 5554  df-cnv 5556  df-xr 10667  df-le 10669
This theorem is referenced by:  ltnle  10708  letri3  10714  leloe  10715  eqlelt  10716  ne0gt0  10733  lelttric  10735  lenlti  10748  lenltd  10774  ltaddsub  11102  leord1  11155  lediv1  11493  suprleub  11595  dfinfre  11610  infregelb  11613  nnge1  11653  nnnlt1  11657  avgle1  11865  avgle2  11866  nn0nlt0  11911  recnz  12045  btwnnz  12046  prime  12051  indstr  12304  uzsupss  12328  zbtwnre  12334  rpneg  12409  2resupmax  12569  fzn  12911  nelfzo  13031  fzonlt0  13048  fllt  13164  flflp1  13165  modifeq2int  13289  om2uzlt2i  13307  fsuppmapnn0fiub0  13349  suppssfz  13350  leexp2  13523  discr  13589  bcval4  13655  ccatsymb  13924  swrd0  14008  sqrtneglem  14614  harmonic  15202  efle  15459  dvdsle  15648  dfgcd2  15882  lcmf  15965  infpnlem1  16234  pgpssslw  18668  gsummoncoe1  20400  mp2pm2mplem4  21345  dvferm1  24509  dvferm2  24511  dgrlt  24783  logleb  25113  argrege0  25121  ellogdm  25149  cxple  25205  cxple3  25211  asinneg  25391  birthdaylem3  25458  ppieq0  25680  chpeq0  25711  chteq0  25712  lgsval2lem  25810  lgsneg  25824  lgsdilem  25827  gausslemma2dlem1a  25868  gausslemma2dlem3  25871  ostth2lem1  26121  ostth3  26141  rusgrnumwwlks  27680  clwlkclwwlklem2a  27703  frgrreg  28100  friendship  28105  nmounbi  28480  nmlno0lem  28497  nmlnop0iALT  29699  supfz  32857  inffz  32858  fz0n  32859  nn0prpw  33568  leceifl  34762  poimirlem15  34788  poimirlem16  34789  poimirlem17  34790  poimirlem20  34793  poimirlem24  34797  poimirlem31  34804  poimirlem32  34805  ftc1anclem1  34848  nninfnub  34907  ellz1  39242  rencldnfilem  39295  limsup10ex  41930  icccncfext  42046  subsubelfzo0  43403  digexp  44595  reorelicc  44625
  Copyright terms: Public domain W3C validator