Theorem lenlt 11388

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2145   class class class wbr 5103  ℝcr 11199  ℝ^*cxr 11342   < clt 11343   ≤ cle 11344

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5657  df-cnv 5659  df-xr 11347  df-le 11349

This theorem is used by:  ltnle  11389  letri3  11395  leloe  11396  eqlelt  11397  ne0gt0  11415  lelttric  11417  lenlti  11430  lenltd  11456  ltaddsub  11790  leord1  11843  lediv1  12182  suprleub  12283  dfinfre  12298  infregelb  12301  nnge1  12366  nnnlt1  12370  avgle1  12586  avgle2  12587  nn0nlt0  12632  recnz  12774  btwnnz  12775  prime  12780  indstr  13043  uzsupss  13067  zbtwnre  13073  rpneg  13154  2resupmax  13318  fzn  13673  nelfzo  13799  fzonlt0  13817  fllt  13946  flflp1  13947  modifeq2int  14076  om2uzlt2i  14094  fsuppmapnn0fiub0  14136  suppssfz  14137  leexp2  14314  discr  14384  bcval4  14451  ccatsymb  14728  swrd0  14808  sqrtneglem  15433  harmonic  16028  efle  16286  dvdsle  16480  dfgcd2  16719  lcmf  16808  infpnlem1  17088  pgpssslw  19828  gsummoncoe1  22626  mp2pm2mplem4  23127  dvferm1  26305  dvferm2  26307  dgrlt  26585  logleb  26931  argrege0  26939  ellogdm  26967  cxple  27023  cxple3  27029  asinneg  27214  birthdaylem3  27281  ppieq0  27503  chpeq0  27535  chteq0  27536  lgsval2lem  27634  lgsneg  27648  lgsdilem  27651  gausslemma2dlem1a  27692  gausslemma2dlem3  27695  ostth2lem1  27945  ostth3  27965  rusgrnumwwlks  30566  clwlkclwwlklem2a  30589  frgrreg  30995  friendship  31000  nmounbi  31378  nmlno0lem  31395  nmlnop0iALT  32597  supfz  36494  inffz  36495  fz0n  36496  nn0prpw  37111  leceifl  38532  poimirlem15  38553  poimirlem16  38554  poimirlem17  38555  poimirlem20  38558  poimirlem24  38562  poimirlem31  38569  poimirlem32  38570  ftc1anclem1  38611  nninfnub  38685  ellz1  43777  rencldnfilem  43826  icccncfext  46896  subsubelfzo0  48396  digexp  49718  reorelicc  49821