Theorem lenlt 11194

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2109   class class class wbr 5092  ℝcr 11008  ℝ^*cxr 11148   < clt 11149   ≤ cle 11150

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-xp 5625  df-cnv 5627  df-xr 11153  df-le 11155

This theorem is referenced by:  ltnle  11195  letri3  11201  leloe  11202  eqlelt  11203  ne0gt0  11221  lelttric  11223  lenlti  11236  lenltd  11262  ltaddsub  11594  leord1  11647  lediv1  11990  suprleub  12091  dfinfre  12106  infregelb  12109  nnge1  12156  nnnlt1  12160  avgle1  12364  avgle2  12365  nn0nlt0  12410  recnz  12551  btwnnz  12552  prime  12557  indstr  12817  uzsupss  12841  zbtwnre  12847  rpneg  12927  2resupmax  13090  fzn  13443  nelfzo  13567  fzonlt0  13585  fllt  13710  flflp1  13711  modifeq2int  13840  om2uzlt2i  13858  fsuppmapnn0fiub0  13900  suppssfz  13901  leexp2  14078  discr  14147  bcval4  14214  ccatsymb  14489  swrd0  14565  sqrtneglem  15173  harmonic  15766  efle  16027  dvdsle  16221  dfgcd2  16457  lcmf  16544  infpnlem1  16822  pgpssslw  19493  gsummoncoe1  22193  mp2pm2mplem4  22694  dvferm1  25887  dvferm2  25889  dgrlt  26170  logleb  26510  argrege0  26518  ellogdm  26546  cxple  26602  cxple3  26608  asinneg  26794  birthdaylem3  26861  ppieq0  27084  chpeq0  27117  chteq0  27118  lgsval2lem  27216  lgsneg  27230  lgsdilem  27233  gausslemma2dlem1a  27274  gausslemma2dlem3  27277  ostth2lem1  27527  ostth3  27547  rusgrnumwwlks  29919  clwlkclwwlklem2a  29942  frgrreg  30338  friendship  30343  nmounbi  30720  nmlno0lem  30737  nmlnop0iALT  31939  supfz  35712  inffz  35713  fz0n  35714  nn0prpw  36307  leceifl  37599  poimirlem15  37625  poimirlem16  37626  poimirlem17  37627  poimirlem20  37630  poimirlem24  37634  poimirlem31  37641  poimirlem32  37642  ftc1anclem1  37683  nninfnub  37741  ellz1  42750  rencldnfilem  42803  icccncfext  45878  subsubelfzo0  47320  digexp  48602  reorelicc  48705