Theorem lenlt 11288

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∈ wcel 2149   class class class wbr 5113  ℝcr 11099  ℝ^*cxr 11242   < clt 11243   ≤ cle 11244

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-opab 5178  df-xp 5668  df-cnv 5670  df-xr 11247  df-le 11249

This theorem is referenced by:  ltnle  11289  letri3  11295  leloe  11296  eqlelt  11297  ne0gt0  11315  lelttric  11317  lenlti  11330  lenltd  11356  ltaddsub  11688  leord1  11741  lediv1  12080  suprleub  12181  dfinfre  12196  infregelb  12199  nnge1  12264  nnnlt1  12268  avgle1  12484  avgle2  12485  nn0nlt0  12530  recnz  12671  btwnnz  12672  prime  12677  indstr  12940  uzsupss  12964  zbtwnre  12970  rpneg  13050  2resupmax  13214  fzn  13568  nelfzo  13693  fzonlt0  13711  fllt  13839  flflp1  13840  modifeq2int  13969  om2uzlt2i  13987  fsuppmapnn0fiub0  14029  suppssfz  14030  leexp2  14207  discr  14276  bcval4  14343  ccatsymb  14620  swrd0  14696  sqrtneglem  15317  harmonic  15913  efle  16174  dvdsle  16368  dfgcd2  16604  lcmf  16691  infpnlem1  16970  pgpssslw  19684  gsummoncoe1  22437  mp2pm2mplem4  22935  dvferm1  26113  dvferm2  26115  dgrlt  26392  logleb  26734  argrege0  26742  ellogdm  26770  cxple  26826  cxple3  26832  asinneg  27017  birthdaylem3  27084  ppieq0  27306  chpeq0  27338  chteq0  27339  lgsval2lem  27437  lgsneg  27451  lgsdilem  27454  gausslemma2dlem1a  27495  gausslemma2dlem3  27498  ostth2lem1  27748  ostth3  27768  rusgrnumwwlks  30267  clwlkclwwlklem2a  30290  frgrreg  30686  friendship  30691  nmounbi  31069  nmlno0lem  31086  nmlnop0iALT  32288  supfz  36154  inffz  36155  fz0n  36156  nn0prpw  36757  leceifl  38182  poimirlem15  38208  poimirlem16  38209  poimirlem17  38210  poimirlem20  38213  poimirlem24  38217  poimirlem31  38224  poimirlem32  38225  ftc1anclem1  38266  nninfnub  38324  ellz1  43424  rencldnfilem  43473  icccncfext  46527  subsubelfzo0  47987  digexp  49306  reorelicc  49409