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

Theorem lenlt 10410
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 10379 . 2 (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
2 rexr 10379 . 2 (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*)
3 xrlenlt 10397 . 2 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))
41, 2, 3syl2an 585 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wcel 2157   class class class wbr 4855  cr 10229  *cxr 10367   < clt 10368  cle 10369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-sep 4988  ax-nul 4996  ax-pr 5109
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3404  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-sn 4382  df-pr 4384  df-op 4388  df-br 4856  df-opab 4918  df-xp 5330  df-cnv 5332  df-xr 10372  df-le 10374
This theorem is referenced by:  ltnle  10411  letri3  10417  leloe  10418  eqlelt  10419  ne0gt0  10436  lelttric  10438  lenlti  10451  lenltd  10477  ltaddsub  10796  leord1  10849  lediv1  11182  suprleub  11283  dfinfre  11298  infregelb  11301  nnge1  11343  nnnlt1  11347  avgle1  11558  avgle2  11559  nn0nlt0  11604  recnz  11737  btwnnz  11738  prime  11743  indstr  11994  uzsupss  12018  zbtwnre  12024  rpneg  12096  2resupmax  12256  fzn  12599  nelfzo  12718  fzonlt0  12734  fllt  12850  flflp1  12851  modifeq2int  12975  om2uzlt2i  12993  fsuppmapnn0fiub0  13035  suppssfz  13036  leexp2  13157  discr  13243  bcval4  13333  ccatsymb  13598  swrd0  13677  sqrtneglem  14249  harmonic  14832  efle  15087  dvdsle  15274  dfgcd2  15501  lcmf  15584  infpnlem1  15850  pgpssslw  18249  gsummoncoe1  19901  mp2pm2mplem4  20847  dvferm1  23984  dvferm2  23986  dgrlt  24258  logleb  24585  argrege0  24593  ellogdm  24621  dvlog2lem  24634  cxple  24677  cxple3  24683  asinneg  24849  birthdaylem3  24916  ppieq0  25138  chpeq0  25169  chteq0  25170  lgsval2lem  25268  lgsneg  25282  lgsdilem  25285  gausslemma2dlem1a  25326  gausslemma2dlem3  25329  ostth2lem1  25543  ostth3  25563  upgrewlkle2  26752  rusgrnumwwlks  27138  clwlkclwwlklem2a  27163  frgrreg  27604  friendship  27609  nmounbi  27981  nmlno0lem  27998  nmlnop0iALT  29204  supfz  31956  inffz  31957  inffzOLD  31958  fz0n  31959  nn0prpw  32660  leceifl  33729  poimirlem15  33755  poimirlem16  33756  poimirlem17  33757  poimirlem20  33760  poimirlem24  33764  poimirlem31  33771  poimirlem32  33772  ftc1anclem1  33815  nninfnub  33876  ellz1  37849  rencldnfilem  37903  limsup10ex  40502  icccncfext  40597  subsubelfzo0  41928  digexp  42986
  Copyright terms: Public domain W3C validator