Theorem lenlt 11307

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2146   class class class wbr 5111  ℝcr 11118  ℝ^*cxr 11261   < clt 11262   ≤ cle 11263

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 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

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 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-xp 5669  df-cnv 5671  df-xr 11266  df-le 11268

This theorem is used by:  ltnle  11308  letri3  11314  leloe  11315  eqlelt  11316  ne0gt0  11334  lelttric  11336  lenlti  11349  lenltd  11375  ltaddsub  11707  leord1  11760  lediv1  12099  suprleub  12200  dfinfre  12215  infregelb  12218  nnge1  12283  nnnlt1  12287  avgle1  12503  avgle2  12504  nn0nlt0  12549  recnz  12691  btwnnz  12692  prime  12697  indstr  12960  uzsupss  12984  zbtwnre  12990  rpneg  13070  2resupmax  13234  fzn  13588  nelfzo  13714  fzonlt0  13732  fllt  13861  flflp1  13862  modifeq2int  13991  om2uzlt2i  14009  fsuppmapnn0fiub0  14051  suppssfz  14052  leexp2  14229  discr  14298  bcval4  14365  ccatsymb  14642  swrd0  14722  sqrtneglem  15345  harmonic  15940  efle  16200  dvdsle  16394  dfgcd2  16630  lcmf  16717  infpnlem1  16996  pgpssslw  19732  gsummoncoe1  22522  mp2pm2mplem4  23020  dvferm1  26199  dvferm2  26201  dgrlt  26478  logleb  26823  argrege0  26831  ellogdm  26859  cxple  26915  cxple3  26921  asinneg  27106  birthdaylem3  27173  ppieq0  27395  chpeq0  27427  chteq0  27428  lgsval2lem  27526  lgsneg  27540  lgsdilem  27543  gausslemma2dlem1a  27584  gausslemma2dlem3  27587  ostth2lem1  27837  ostth3  27857  rusgrnumwwlks  30397  clwlkclwwlklem2a  30420  frgrreg  30820  friendship  30825  nmounbi  31203  nmlno0lem  31220  nmlnop0iALT  32422  supfz  36262  inffz  36263  fz0n  36264  nn0prpw  36895  leceifl  38321  poimirlem15  38347  poimirlem16  38348  poimirlem17  38349  poimirlem20  38352  poimirlem24  38356  poimirlem31  38363  poimirlem32  38364  ftc1anclem1  38405  nninfnub  38464  ellz1  43575  rencldnfilem  43624  icccncfext  46678  subsubelfzo0  48141  digexp  49463  reorelicc  49566