Theorem lenlt 11315

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 11282	. 2 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
2		rexr 11282	. 2 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*)
3		xrlenlt 11301	. 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 11126  ℝ^*cxr 11269   < clt 11270   ≤ cle 11271

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 2732  ax-sep 5251  ax-pr 5398

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 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  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 5661  df-cnv 5663  df-xr 11274  df-le 11276

This theorem is used by:  ltnle  11316  letri3  11322  leloe  11323  eqlelt  11324  ne0gt0  11342  lelttric  11344  lenlti  11357  lenltd  11383  ltaddsub  11715  leord1  11768  lediv1  12107  suprleub  12208  dfinfre  12223  infregelb  12226  nnge1  12291  nnnlt1  12295  avgle1  12511  avgle2  12512  nn0nlt0  12557  recnz  12699  btwnnz  12700  prime  12705  indstr  12968  uzsupss  12992  zbtwnre  12998  rpneg  13079  2resupmax  13243  fzn  13597  nelfzo  13723  fzonlt0  13741  fllt  13870  flflp1  13871  modifeq2int  14000  om2uzlt2i  14018  fsuppmapnn0fiub0  14060  suppssfz  14061  leexp2  14238  discr  14307  bcval4  14374  ccatsymb  14651  swrd0  14731  sqrtneglem  15356  harmonic  15951  efle  16209  dvdsle  16403  dfgcd2  16639  lcmf  16726  infpnlem1  17005  pgpssslw  19744  gsummoncoe1  22536  mp2pm2mplem4  23037  dvferm1  26215  dvferm2  26217  dgrlt  26495  logleb  26843  argrege0  26851  ellogdm  26879  cxple  26935  cxple3  26941  asinneg  27126  birthdaylem3  27193  ppieq0  27415  chpeq0  27447  chteq0  27448  lgsval2lem  27546  lgsneg  27560  lgsdilem  27563  gausslemma2dlem1a  27604  gausslemma2dlem3  27607  ostth2lem1  27857  ostth3  27877  rusgrnumwwlks  30448  clwlkclwwlklem2a  30471  frgrreg  30877  friendship  30882  nmounbi  31260  nmlno0lem  31277  nmlnop0iALT  32479  supfz  36311  inffz  36312  fz0n  36313  nn0prpw  36945  leceifl  38366  poimirlem15  38387  poimirlem16  38388  poimirlem17  38389  poimirlem20  38392  poimirlem24  38396  poimirlem31  38403  poimirlem32  38404  ftc1anclem1  38445  nninfnub  38504  ellz1  43615  rencldnfilem  43664  icccncfext  46718  subsubelfzo0  48218  digexp  49540  reorelicc  49643