Theorem lenlt 11209

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2113   class class class wbr 5096  ℝcr 11023  ℝ^*cxr 11163   < clt 11164   ≤ cle 11165

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 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

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 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-opab 5159  df-xp 5628  df-cnv 5630  df-xr 11168  df-le 11170

This theorem is referenced by:  ltnle  11210  letri3  11216  leloe  11217  eqlelt  11218  ne0gt0  11236  lelttric  11238  lenlti  11251  lenltd  11277  ltaddsub  11609  leord1  11662  lediv1  12005  suprleub  12106  dfinfre  12121  infregelb  12124  nnge1  12171  nnnlt1  12175  avgle1  12379  avgle2  12380  nn0nlt0  12425  recnz  12565  btwnnz  12566  prime  12571  indstr  12827  uzsupss  12851  zbtwnre  12857  rpneg  12937  2resupmax  13101  fzn  13454  nelfzo  13578  fzonlt0  13596  fllt  13724  flflp1  13725  modifeq2int  13854  om2uzlt2i  13872  fsuppmapnn0fiub0  13914  suppssfz  13915  leexp2  14092  discr  14161  bcval4  14228  ccatsymb  14504  swrd0  14580  sqrtneglem  15187  harmonic  15780  efle  16041  dvdsle  16235  dfgcd2  16471  lcmf  16558  infpnlem1  16836  pgpssslw  19541  gsummoncoe1  22250  mp2pm2mplem4  22751  dvferm1  25943  dvferm2  25945  dgrlt  26226  logleb  26566  argrege0  26574  ellogdm  26602  cxple  26658  cxple3  26664  asinneg  26850  birthdaylem3  26917  ppieq0  27140  chpeq0  27173  chteq0  27174  lgsval2lem  27272  lgsneg  27286  lgsdilem  27289  gausslemma2dlem1a  27330  gausslemma2dlem3  27333  ostth2lem1  27583  ostth3  27603  rusgrnumwwlks  29999  clwlkclwwlklem2a  30022  frgrreg  30418  friendship  30423  nmounbi  30800  nmlno0lem  30817  nmlnop0iALT  32019  supfz  35872  inffz  35873  fz0n  35874  nn0prpw  36466  leceifl  37749  poimirlem15  37775  poimirlem16  37776  poimirlem17  37777  poimirlem20  37780  poimirlem24  37784  poimirlem31  37791  poimirlem32  37792  ftc1anclem1  37833  nninfnub  37891  ellz1  42951  rencldnfilem  43004  icccncfext  46073  subsubelfzo0  47514  digexp  48795  reorelicc  48898