Theorem lenlt 11216

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

Step	Hyp	Ref	Expression
1		rexr 11183	. 2 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
2		rexr 11183	. 2 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*)
3		xrlenlt 11202	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))
4	1, 2, 3	syl2an 602	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   ∈ wcel 2119   class class class wbr 5073  ℝcr 11029  ℝ^*cxr 11170   < clt 11171   ≤ cle 11172

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5219  ax-pr 5363

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4263  df-if 4456  df-sn 4557  df-pr 4559  df-op 4563  df-br 5074  df-opab 5136  df-xp 5625  df-cnv 5627  df-xr 11175  df-le 11177

This theorem is referenced by:  ltnle  11217  letri3  11223  leloe  11224  eqlelt  11225  ne0gt0  11243  lelttric  11245  lenlti  11258  lenltd  11284  ltaddsub  11616  leord1  11669  lediv1  12013  suprleub  12114  dfinfre  12129  infregelb  12132  nnge1  12197  nnnlt1  12201  avgle1  12409  avgle2  12410  nn0nlt0  12455  recnz  12596  btwnnz  12597  prime  12602  indstr  12858  uzsupss  12882  zbtwnre  12888  rpneg  12968  2resupmax  13132  fzn  13486  nelfzo  13611  fzonlt0  13629  fllt  13757  flflp1  13758  modifeq2int  13887  om2uzlt2i  13905  fsuppmapnn0fiub0  13947  suppssfz  13948  leexp2  14125  discr  14194  bcval4  14261  ccatsymb  14537  swrd0  14613  sqrtneglem  15220  harmonic  15816  efle  16077  dvdsle  16271  dfgcd2  16507  lcmf  16594  infpnlem1  16873  pgpssslw  19581  gsummoncoe1  22295  mp2pm2mplem4  22793  dvferm1  25971  dvferm2  25973  dgrlt  26250  logleb  26586  argrege0  26594  ellogdm  26622  cxple  26678  cxple3  26684  asinneg  26869  birthdaylem3  26936  ppieq0  27158  chpeq0  27190  chteq0  27191  lgsval2lem  27289  lgsneg  27303  lgsdilem  27306  gausslemma2dlem1a  27347  gausslemma2dlem3  27350  ostth2lem1  27600  ostth3  27620  rusgrnumwwlks  30064  clwlkclwwlklem2a  30087  frgrreg  30483  friendship  30488  nmounbi  30866  nmlno0lem  30883  nmlnop0iALT  32085  supfz  35966  inffz  35967  fz0n  35968  nn0prpw  36560  leceifl  37985  poimirlem15  38011  poimirlem16  38012  poimirlem17  38013  poimirlem20  38016  poimirlem24  38020  poimirlem31  38027  poimirlem32  38028  ftc1anclem1  38069  nninfnub  38127  ellz1  43225  rencldnfilem  43274  icccncfext  46338  subsubelfzo0  47798  digexp  49106  reorelicc  49209