Theorem lenlt 11225

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2114   class class class wbr 5100  ℝcr 11039  ℝ^*cxr 11179   < clt 11180   ≤ cle 11181

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 5245  ax-pr 5381

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5640  df-cnv 5642  df-xr 11184  df-le 11186

This theorem is referenced by:  ltnle  11226  letri3  11232  leloe  11233  eqlelt  11234  ne0gt0  11252  lelttric  11254  lenlti  11267  lenltd  11293  ltaddsub  11625  leord1  11678  lediv1  12021  suprleub  12122  dfinfre  12137  infregelb  12140  nnge1  12187  nnnlt1  12191  avgle1  12395  avgle2  12396  nn0nlt0  12441  recnz  12581  btwnnz  12582  prime  12587  indstr  12843  uzsupss  12867  zbtwnre  12873  rpneg  12953  2resupmax  13117  fzn  13470  nelfzo  13594  fzonlt0  13612  fllt  13740  flflp1  13741  modifeq2int  13870  om2uzlt2i  13888  fsuppmapnn0fiub0  13930  suppssfz  13931  leexp2  14108  discr  14177  bcval4  14244  ccatsymb  14520  swrd0  14596  sqrtneglem  15203  harmonic  15796  efle  16057  dvdsle  16251  dfgcd2  16487  lcmf  16574  infpnlem1  16852  pgpssslw  19560  gsummoncoe1  22269  mp2pm2mplem4  22770  dvferm1  25962  dvferm2  25964  dgrlt  26245  logleb  26585  argrege0  26593  ellogdm  26621  cxple  26677  cxple3  26683  asinneg  26869  birthdaylem3  26936  ppieq0  27159  chpeq0  27192  chteq0  27193  lgsval2lem  27291  lgsneg  27305  lgsdilem  27308  gausslemma2dlem1a  27349  gausslemma2dlem3  27352  ostth2lem1  27602  ostth3  27622  rusgrnumwwlks  30068  clwlkclwwlklem2a  30091  frgrreg  30487  friendship  30492  nmounbi  30870  nmlno0lem  30887  nmlnop0iALT  32089  supfz  35951  inffz  35952  fz0n  35953  nn0prpw  36545  leceifl  37889  poimirlem15  37915  poimirlem16  37916  poimirlem17  37917  poimirlem20  37920  poimirlem24  37924  poimirlem31  37931  poimirlem32  37932  ftc1anclem1  37973  nninfnub  38031  ellz1  43153  rencldnfilem  43206  icccncfext  46274  subsubelfzo0  47715  digexp  48996  reorelicc  49099