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

Theorem lenlt 10060
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 10029 . 2 (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
2 rexr 10029 . 2 (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*)
3 xrlenlt 10047 . 2 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))
41, 2, 3syl2an 494 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  wcel 1987   class class class wbr 4613  cr 9879  *cxr 10017   < clt 10018  cle 10019
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pr 4867
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-br 4614  df-opab 4674  df-xp 5080  df-cnv 5082  df-xr 10022  df-le 10024
This theorem is referenced by:  ltnle  10061  letri3  10067  leloe  10068  eqlelt  10069  ne0gt0  10086  lelttric  10088  lenlti  10101  lenltd  10127  ltaddsub  10446  leord1  10499  lediv1  10832  suprleub  10933  dfinfre  10948  infregelb  10951  nnge1  10990  nnnlt1  10994  avgle1  11216  avgle2  11217  nn0nlt0  11263  recnz  11396  btwnnz  11397  prime  11402  indstr  11700  uzsupss  11724  zbtwnre  11730  rpneg  11807  2resupmax  11962  fzn  12299  nelfzo  12416  fzonlt0  12432  fllt  12547  flflp1  12548  modifeq2int  12672  om2uzlt2i  12690  fsuppmapnn0fiub0  12733  suppssfz  12734  leexp2  12855  discr  12941  bcval4  13034  ccatsymb  13305  swrd0  13372  sqrtneglem  13941  harmonic  14516  efle  14773  dvdsle  14956  dfgcd2  15187  lcmf  15270  infpnlem1  15538  pgpssslw  17950  gsummoncoe1  19593  mp2pm2mplem4  20533  dvferm1  23652  dvferm2  23654  dgrlt  23926  logleb  24253  argrege0  24261  ellogdm  24285  dvlog2lem  24298  cxple  24341  cxple3  24347  asinneg  24513  birthdaylem3  24580  ppieq0  24802  chpeq0  24833  chteq0  24834  lgsval2lem  24932  lgsneg  24946  lgsdilem  24949  gausslemma2dlem1a  24990  gausslemma2dlem3  24993  ostth2lem1  25207  ostth3  25227  upgrewlkle2  26372  rusgrnumwwlks  26736  clwlkclwwlklem2a  26766  frgrreg  27106  friendship  27111  nmounbi  27480  nmlno0lem  27497  nmlnop0iALT  28703  supfz  31321  inffz  31322  inffzOLD  31323  fz0n  31324  nn0prpw  31960  leceifl  33030  poimirlem15  33056  poimirlem16  33057  poimirlem17  33058  poimirlem20  33061  poimirlem24  33065  poimirlem31  33072  poimirlem32  33073  ftc1anclem1  33117  nninfnub  33179  ellz1  36810  rencldnfilem  36864  icccncfext  39404  subsubelfzo0  40633  digexp  41693
  Copyright terms: Public domain W3C validator