Theorem lenlt 11191

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 11158	. 2 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
2		rexr 11158	. 2 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*)
3		xrlenlt 11177	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))
4	1, 2, 3	syl2an 596	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2111   class class class wbr 5089  ℝcr 11005  ℝ^*cxr 11145   < clt 11146   ≤ cle 11147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090  df-opab 5152  df-xp 5620  df-cnv 5622  df-xr 11150  df-le 11152

This theorem is referenced by:  ltnle  11192  letri3  11198  leloe  11199  eqlelt  11200  ne0gt0  11218  lelttric  11220  lenlti  11233  lenltd  11259  ltaddsub  11591  leord1  11644  lediv1  11987  suprleub  12088  dfinfre  12103  infregelb  12106  nnge1  12153  nnnlt1  12157  avgle1  12361  avgle2  12362  nn0nlt0  12407  recnz  12548  btwnnz  12549  prime  12554  indstr  12814  uzsupss  12838  zbtwnre  12844  rpneg  12924  2resupmax  13087  fzn  13440  nelfzo  13564  fzonlt0  13582  fllt  13710  flflp1  13711  modifeq2int  13840  om2uzlt2i  13858  fsuppmapnn0fiub0  13900  suppssfz  13901  leexp2  14078  discr  14147  bcval4  14214  ccatsymb  14490  swrd0  14566  sqrtneglem  15173  harmonic  15766  efle  16027  dvdsle  16221  dfgcd2  16457  lcmf  16544  infpnlem1  16822  pgpssslw  19526  gsummoncoe1  22223  mp2pm2mplem4  22724  dvferm1  25916  dvferm2  25918  dgrlt  26199  logleb  26539  argrege0  26547  ellogdm  26575  cxple  26631  cxple3  26637  asinneg  26823  birthdaylem3  26890  ppieq0  27113  chpeq0  27146  chteq0  27147  lgsval2lem  27245  lgsneg  27259  lgsdilem  27262  gausslemma2dlem1a  27303  gausslemma2dlem3  27306  ostth2lem1  27556  ostth3  27576  rusgrnumwwlks  29955  clwlkclwwlklem2a  29978  frgrreg  30374  friendship  30379  nmounbi  30756  nmlno0lem  30773  nmlnop0iALT  31975  supfz  35773  inffz  35774  fz0n  35775  nn0prpw  36367  leceifl  37648  poimirlem15  37674  poimirlem16  37675  poimirlem17  37676  poimirlem20  37679  poimirlem24  37683  poimirlem31  37690  poimirlem32  37691  ftc1anclem1  37732  nninfnub  37790  ellz1  42859  rencldnfilem  42912  icccncfext  45984  subsubelfzo0  47425  digexp  48707  reorelicc  48810