Theorem lenlt 11339

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2108   class class class wbr 5143  ℝcr 11154  ℝ^*cxr 11294   < clt 11295   ≤ cle 11296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691  df-cnv 5693  df-xr 11299  df-le 11301

This theorem is referenced by:  ltnle  11340  letri3  11346  leloe  11347  eqlelt  11348  ne0gt0  11366  lelttric  11368  lenlti  11381  lenltd  11407  ltaddsub  11737  leord1  11790  lediv1  12133  suprleub  12234  dfinfre  12249  infregelb  12252  nnge1  12294  nnnlt1  12298  avgle1  12506  avgle2  12507  nn0nlt0  12552  recnz  12693  btwnnz  12694  prime  12699  indstr  12958  uzsupss  12982  zbtwnre  12988  rpneg  13067  2resupmax  13230  fzn  13580  nelfzo  13704  fzonlt0  13722  fllt  13846  flflp1  13847  modifeq2int  13974  om2uzlt2i  13992  fsuppmapnn0fiub0  14034  suppssfz  14035  leexp2  14211  discr  14279  bcval4  14346  ccatsymb  14620  swrd0  14696  sqrtneglem  15305  harmonic  15895  efle  16154  dvdsle  16347  dfgcd2  16583  lcmf  16670  infpnlem1  16948  pgpssslw  19632  gsummoncoe1  22312  mp2pm2mplem4  22815  dvferm1  26023  dvferm2  26025  dgrlt  26306  logleb  26645  argrege0  26653  ellogdm  26681  cxple  26737  cxple3  26743  asinneg  26929  birthdaylem3  26996  ppieq0  27219  chpeq0  27252  chteq0  27253  lgsval2lem  27351  lgsneg  27365  lgsdilem  27368  gausslemma2dlem1a  27409  gausslemma2dlem3  27412  ostth2lem1  27662  ostth3  27682  rusgrnumwwlks  29994  clwlkclwwlklem2a  30017  frgrreg  30413  friendship  30418  nmounbi  30795  nmlno0lem  30812  nmlnop0iALT  32014  supfz  35729  inffz  35730  fz0n  35731  nn0prpw  36324  leceifl  37616  poimirlem15  37642  poimirlem16  37643  poimirlem17  37644  poimirlem20  37647  poimirlem24  37651  poimirlem31  37658  poimirlem32  37659  ftc1anclem1  37700  nninfnub  37758  metakunt22  42227  ellz1  42778  rencldnfilem  42831  icccncfext  45902  subsubelfzo0  47338  digexp  48528  reorelicc  48631