Theorem lenlt 11311

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 11279	. 2 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
2		rexr 11279	. 2 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*)
3		xrlenlt 11298	. 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 11126  ℝ^*cxr 11266   < clt 11267   ≤ cle 11268

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 11271  df-le 11273

This theorem is referenced by:  ltnle  11312  letri3  11318  leloe  11319  eqlelt  11320  ne0gt0  11338  lelttric  11340  lenlti  11353  lenltd  11379  ltaddsub  11709  leord1  11762  lediv1  12105  suprleub  12206  dfinfre  12221  infregelb  12224  nnge1  12266  nnnlt1  12270  avgle1  12479  avgle2  12480  nn0nlt0  12525  recnz  12666  btwnnz  12667  prime  12672  indstr  12930  uzsupss  12954  zbtwnre  12960  rpneg  13039  2resupmax  13202  fzn  13555  nelfzo  13679  fzonlt0  13697  fllt  13821  flflp1  13822  modifeq2int  13949  om2uzlt2i  13967  fsuppmapnn0fiub0  14009  suppssfz  14010  leexp2  14187  discr  14256  bcval4  14323  ccatsymb  14598  swrd0  14674  sqrtneglem  15283  harmonic  15873  efle  16134  dvdsle  16327  dfgcd2  16563  lcmf  16650  infpnlem1  16928  pgpssslw  19593  gsummoncoe1  22244  mp2pm2mplem4  22745  dvferm1  25939  dvferm2  25941  dgrlt  26222  logleb  26562  argrege0  26570  ellogdm  26598  cxple  26654  cxple3  26660  asinneg  26846  birthdaylem3  26913  ppieq0  27136  chpeq0  27169  chteq0  27170  lgsval2lem  27268  lgsneg  27282  lgsdilem  27285  gausslemma2dlem1a  27326  gausslemma2dlem3  27329  ostth2lem1  27579  ostth3  27599  rusgrnumwwlks  29902  clwlkclwwlklem2a  29925  frgrreg  30321  friendship  30326  nmounbi  30703  nmlno0lem  30720  nmlnop0iALT  31922  supfz  35692  inffz  35693  fz0n  35694  nn0prpw  36287  leceifl  37579  poimirlem15  37605  poimirlem16  37606  poimirlem17  37607  poimirlem20  37610  poimirlem24  37614  poimirlem31  37621  poimirlem32  37622  ftc1anclem1  37663  nninfnub  37721  metakunt22  42185  ellz1  42737  rencldnfilem  42790  icccncfext  45864  subsubelfzo0  47303  digexp  48535  reorelicc  48638