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

Theorem lenlt 10328
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 10297 . 2 (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
2 rexr 10297 . 2 (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*)
3 xrlenlt 10315 . 2 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))
41, 2, 3syl2an 495 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  wcel 2139   class class class wbr 4804  cr 10147  *cxr 10285   < clt 10286  cle 10287
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pr 5055
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-br 4805  df-opab 4865  df-xp 5272  df-cnv 5274  df-xr 10290  df-le 10292
This theorem is referenced by:  ltnle  10329  letri3  10335  leloe  10336  eqlelt  10337  ne0gt0  10354  lelttric  10356  lenlti  10369  lenltd  10395  ltaddsub  10714  leord1  10767  lediv1  11100  suprleub  11201  dfinfre  11216  infregelb  11219  nnge1  11258  nnnlt1  11262  avgle1  11484  avgle2  11485  nn0nlt0  11531  recnz  11664  btwnnz  11665  prime  11670  indstr  11969  uzsupss  11993  zbtwnre  11999  rpneg  12076  2resupmax  12232  fzn  12570  nelfzo  12689  fzonlt0  12705  fllt  12821  flflp1  12822  modifeq2int  12946  om2uzlt2i  12964  fsuppmapnn0fiub0  13007  suppssfz  13008  leexp2  13129  discr  13215  bcval4  13308  ccatsymb  13574  swrd0  13654  sqrtneglem  14226  harmonic  14810  efle  15067  dvdsle  15254  dfgcd2  15485  lcmf  15568  infpnlem1  15836  pgpssslw  18249  gsummoncoe1  19896  mp2pm2mplem4  20836  dvferm1  23967  dvferm2  23969  dgrlt  24241  logleb  24569  argrege0  24577  ellogdm  24605  dvlog2lem  24618  cxple  24661  cxple3  24667  asinneg  24833  birthdaylem3  24900  ppieq0  25122  chpeq0  25153  chteq0  25154  lgsval2lem  25252  lgsneg  25266  lgsdilem  25269  gausslemma2dlem1a  25310  gausslemma2dlem3  25313  ostth2lem1  25527  ostth3  25547  upgrewlkle2  26733  rusgrnumwwlks  27117  clwlkclwwlklem2a  27142  frgrreg  27583  friendship  27588  nmounbi  27961  nmlno0lem  27978  nmlnop0iALT  29184  supfz  31941  inffz  31942  inffzOLD  31943  fz0n  31944  nn0prpw  32645  leceifl  33729  poimirlem15  33755  poimirlem16  33756  poimirlem17  33757  poimirlem20  33760  poimirlem24  33764  poimirlem31  33771  poimirlem32  33772  ftc1anclem1  33816  nninfnub  33878  ellz1  37850  rencldnfilem  37904  limsup10ex  40526  icccncfext  40621  subsubelfzo0  41864  digexp  42929
  Copyright terms: Public domain W3C validator