Theorem lenlt 11259

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2109   class class class wbr 5110  ℝcr 11074  ℝ^*cxr 11214   < clt 11215   ≤ cle 11216

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-xp 5647  df-cnv 5649  df-xr 11219  df-le 11221

This theorem is referenced by:  ltnle  11260  letri3  11266  leloe  11267  eqlelt  11268  ne0gt0  11286  lelttric  11288  lenlti  11301  lenltd  11327  ltaddsub  11659  leord1  11712  lediv1  12055  suprleub  12156  dfinfre  12171  infregelb  12174  nnge1  12221  nnnlt1  12225  avgle1  12429  avgle2  12430  nn0nlt0  12475  recnz  12616  btwnnz  12617  prime  12622  indstr  12882  uzsupss  12906  zbtwnre  12912  rpneg  12992  2resupmax  13155  fzn  13508  nelfzo  13632  fzonlt0  13650  fllt  13775  flflp1  13776  modifeq2int  13905  om2uzlt2i  13923  fsuppmapnn0fiub0  13965  suppssfz  13966  leexp2  14143  discr  14212  bcval4  14279  ccatsymb  14554  swrd0  14630  sqrtneglem  15239  harmonic  15832  efle  16093  dvdsle  16287  dfgcd2  16523  lcmf  16610  infpnlem1  16888  pgpssslw  19551  gsummoncoe1  22202  mp2pm2mplem4  22703  dvferm1  25896  dvferm2  25898  dgrlt  26179  logleb  26519  argrege0  26527  ellogdm  26555  cxple  26611  cxple3  26617  asinneg  26803  birthdaylem3  26870  ppieq0  27093  chpeq0  27126  chteq0  27127  lgsval2lem  27225  lgsneg  27239  lgsdilem  27242  gausslemma2dlem1a  27283  gausslemma2dlem3  27286  ostth2lem1  27536  ostth3  27556  rusgrnumwwlks  29911  clwlkclwwlklem2a  29934  frgrreg  30330  friendship  30335  nmounbi  30712  nmlno0lem  30729  nmlnop0iALT  31931  supfz  35723  inffz  35724  fz0n  35725  nn0prpw  36318  leceifl  37610  poimirlem15  37636  poimirlem16  37637  poimirlem17  37638  poimirlem20  37641  poimirlem24  37645  poimirlem31  37652  poimirlem32  37653  ftc1anclem1  37694  nninfnub  37752  ellz1  42762  rencldnfilem  42815  icccncfext  45892  subsubelfzo0  47331  digexp  48600  reorelicc  48703