Theorem lenlt 11054

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∈ wcel 2110   class class class wbr 5079  ℝcr 10871  ℝ^*cxr 11009   < clt 11010   ≤ cle 11011

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-ral 3071  df-rex 3072  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-br 5080  df-opab 5142  df-xp 5596  df-cnv 5598  df-xr 11014  df-le 11016

This theorem is referenced by:  ltnle  11055  letri3  11061  leloe  11062  eqlelt  11063  ne0gt0  11080  lelttric  11082  lenlti  11095  lenltd  11121  ltaddsub  11449  leord1  11502  lediv1  11840  suprleub  11941  dfinfre  11956  infregelb  11959  nnge1  12001  nnnlt1  12005  avgle1  12213  avgle2  12214  nn0nlt0  12259  recnz  12395  btwnnz  12396  prime  12401  indstr  12655  uzsupss  12679  zbtwnre  12685  rpneg  12761  2resupmax  12921  fzn  13271  nelfzo  13391  fzonlt0  13408  fllt  13524  flflp1  13525  modifeq2int  13651  om2uzlt2i  13669  fsuppmapnn0fiub0  13711  suppssfz  13712  leexp2  13887  discr  13953  bcval4  14019  ccatsymb  14285  swrd0  14369  sqrtneglem  14976  harmonic  15569  efle  15825  dvdsle  16017  dfgcd2  16252  lcmf  16336  infpnlem1  16609  pgpssslw  19217  gsummoncoe1  21473  mp2pm2mplem4  21956  dvferm1  25147  dvferm2  25149  dgrlt  25425  logleb  25756  argrege0  25764  ellogdm  25792  cxple  25848  cxple3  25854  asinneg  26034  birthdaylem3  26101  ppieq0  26323  chpeq0  26354  chteq0  26355  lgsval2lem  26453  lgsneg  26467  lgsdilem  26470  gausslemma2dlem1a  26511  gausslemma2dlem3  26514  ostth2lem1  26764  ostth3  26784  rusgrnumwwlks  28335  clwlkclwwlklem2a  28358  frgrreg  28754  friendship  28759  nmounbi  29134  nmlno0lem  29151  nmlnop0iALT  30353  supfz  33690  inffz  33691  fz0n  33692  nn0prpw  34508  leceifl  35762  poimirlem15  35788  poimirlem16  35789  poimirlem17  35790  poimirlem20  35793  poimirlem24  35797  poimirlem31  35804  poimirlem32  35805  ftc1anclem1  35846  nninfnub  35905  metakunt22  40143  ellz1  40586  rencldnfilem  40639  icccncfext  43399  subsubelfzo0  44787  digexp  45922  reorelicc  46025