Theorem lenlt 11219

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2114   class class class wbr 5086  ℝcr 11032  ℝ^*cxr 11173   < clt 11174   ≤ cle 11175

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-xp 5632  df-cnv 5634  df-xr 11178  df-le 11180

This theorem is referenced by:  ltnle  11220  letri3  11226  leloe  11227  eqlelt  11228  ne0gt0  11246  lelttric  11248  lenlti  11261  lenltd  11287  ltaddsub  11619  leord1  11672  lediv1  12016  suprleub  12117  dfinfre  12132  infregelb  12135  nnge1  12200  nnnlt1  12204  avgle1  12412  avgle2  12413  nn0nlt0  12458  recnz  12599  btwnnz  12600  prime  12605  indstr  12861  uzsupss  12885  zbtwnre  12891  rpneg  12971  2resupmax  13135  fzn  13489  nelfzo  13614  fzonlt0  13632  fllt  13760  flflp1  13761  modifeq2int  13890  om2uzlt2i  13908  fsuppmapnn0fiub0  13950  suppssfz  13951  leexp2  14128  discr  14197  bcval4  14264  ccatsymb  14540  swrd0  14616  sqrtneglem  15223  harmonic  15819  efle  16080  dvdsle  16274  dfgcd2  16510  lcmf  16597  infpnlem1  16876  pgpssslw  19584  gsummoncoe1  22287  mp2pm2mplem4  22788  dvferm1  25966  dvferm2  25968  dgrlt  26245  logleb  26584  argrege0  26592  ellogdm  26620  cxple  26676  cxple3  26682  asinneg  26867  birthdaylem3  26934  ppieq0  27157  chpeq0  27189  chteq0  27190  lgsval2lem  27288  lgsneg  27302  lgsdilem  27305  gausslemma2dlem1a  27346  gausslemma2dlem3  27349  ostth2lem1  27599  ostth3  27619  rusgrnumwwlks  30064  clwlkclwwlklem2a  30087  frgrreg  30483  friendship  30488  nmounbi  30866  nmlno0lem  30883  nmlnop0iALT  32085  supfz  35931  inffz  35932  fz0n  35933  nn0prpw  36525  leceifl  37948  poimirlem15  37974  poimirlem16  37975  poimirlem17  37976  poimirlem20  37979  poimirlem24  37983  poimirlem31  37990  poimirlem32  37991  ftc1anclem1  38032  nninfnub  38090  ellz1  43217  rencldnfilem  43270  icccncfext  46337  subsubelfzo0  47791  digexp  49099  reorelicc  49202