Theorem lenlt 11313

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2108   class class class wbr 5119  ℝcr 11128  ℝ^*cxr 11268   < clt 11269   ≤ cle 11270

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 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-xp 5660  df-cnv 5662  df-xr 11273  df-le 11275

This theorem is referenced by:  ltnle  11314  letri3  11320  leloe  11321  eqlelt  11322  ne0gt0  11340  lelttric  11342  lenlti  11355  lenltd  11381  ltaddsub  11711  leord1  11764  lediv1  12107  suprleub  12208  dfinfre  12223  infregelb  12226  nnge1  12268  nnnlt1  12272  avgle1  12481  avgle2  12482  nn0nlt0  12527  recnz  12668  btwnnz  12669  prime  12674  indstr  12932  uzsupss  12956  zbtwnre  12962  rpneg  13041  2resupmax  13204  fzn  13557  nelfzo  13681  fzonlt0  13699  fllt  13823  flflp1  13824  modifeq2int  13951  om2uzlt2i  13969  fsuppmapnn0fiub0  14011  suppssfz  14012  leexp2  14189  discr  14258  bcval4  14325  ccatsymb  14600  swrd0  14676  sqrtneglem  15285  harmonic  15875  efle  16136  dvdsle  16329  dfgcd2  16565  lcmf  16652  infpnlem1  16930  pgpssslw  19595  gsummoncoe1  22246  mp2pm2mplem4  22747  dvferm1  25941  dvferm2  25943  dgrlt  26224  logleb  26564  argrege0  26572  ellogdm  26600  cxple  26656  cxple3  26662  asinneg  26848  birthdaylem3  26915  ppieq0  27138  chpeq0  27171  chteq0  27172  lgsval2lem  27270  lgsneg  27284  lgsdilem  27287  gausslemma2dlem1a  27328  gausslemma2dlem3  27331  ostth2lem1  27581  ostth3  27601  rusgrnumwwlks  29956  clwlkclwwlklem2a  29979  frgrreg  30375  friendship  30380  nmounbi  30757  nmlno0lem  30774  nmlnop0iALT  31976  supfz  35746  inffz  35747  fz0n  35748  nn0prpw  36341  leceifl  37633  poimirlem15  37659  poimirlem16  37660  poimirlem17  37661  poimirlem20  37664  poimirlem24  37668  poimirlem31  37675  poimirlem32  37676  ftc1anclem1  37717  nninfnub  37775  metakunt22  42239  ellz1  42790  rencldnfilem  42843  icccncfext  45916  subsubelfzo0  47355  digexp  48587  reorelicc  48690