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

Theorem lenlt 10712
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 10680 . 2 (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
2 rexr 10680 . 2 (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*)
3 xrlenlt 10699 . 2 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))
41, 2, 3syl2an 598 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wcel 2112   class class class wbr 5033  cr 10529  *cxr 10667   < clt 10668  cle 10669
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pr 5298
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rex 3115  df-v 3446  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-br 5034  df-opab 5096  df-xp 5529  df-cnv 5531  df-xr 10672  df-le 10674
This theorem is referenced by:  ltnle  10713  letri3  10719  leloe  10720  eqlelt  10721  ne0gt0  10738  lelttric  10740  lenlti  10753  lenltd  10779  ltaddsub  11107  leord1  11160  lediv1  11498  suprleub  11598  dfinfre  11613  infregelb  11616  nnge1  11657  nnnlt1  11661  avgle1  11869  avgle2  11870  nn0nlt0  11915  recnz  12049  btwnnz  12050  prime  12055  indstr  12308  uzsupss  12332  zbtwnre  12338  rpneg  12413  2resupmax  12573  fzn  12922  nelfzo  13042  fzonlt0  13059  fllt  13175  flflp1  13176  modifeq2int  13300  om2uzlt2i  13318  fsuppmapnn0fiub0  13360  suppssfz  13361  leexp2  13535  discr  13601  bcval4  13667  ccatsymb  13931  swrd0  14015  sqrtneglem  14621  harmonic  15209  efle  15466  dvdsle  15655  dfgcd2  15887  lcmf  15970  infpnlem1  16239  pgpssslw  18734  gsummoncoe1  20936  mp2pm2mplem4  21417  dvferm1  24591  dvferm2  24593  dgrlt  24866  logleb  25197  argrege0  25205  ellogdm  25233  cxple  25289  cxple3  25295  asinneg  25475  birthdaylem3  25542  ppieq0  25764  chpeq0  25795  chteq0  25796  lgsval2lem  25894  lgsneg  25908  lgsdilem  25911  gausslemma2dlem1a  25952  gausslemma2dlem3  25955  ostth2lem1  26205  ostth3  26225  rusgrnumwwlks  27763  clwlkclwwlklem2a  27786  frgrreg  28182  friendship  28187  nmounbi  28562  nmlno0lem  28579  nmlnop0iALT  29781  supfz  33068  inffz  33069  fz0n  33070  nn0prpw  33779  leceifl  35039  poimirlem15  35065  poimirlem16  35066  poimirlem17  35067  poimirlem20  35070  poimirlem24  35074  poimirlem31  35081  poimirlem32  35082  ftc1anclem1  35123  nninfnub  35182  metakunt22  39362  ellz1  39695  rencldnfilem  39748  icccncfext  42516  subsubelfzo0  43870  digexp  45008  reorelicc  45111
  Copyright terms: Public domain W3C validator