Theorem lenlt 11336

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2105   class class class wbr 5147  ℝcr 11151  ℝ^*cxr 11291   < clt 11292   ≤ cle 11293

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-xp 5694  df-cnv 5696  df-xr 11296  df-le 11298

This theorem is referenced by:  ltnle  11337  letri3  11343  leloe  11344  eqlelt  11345  ne0gt0  11363  lelttric  11365  lenlti  11378  lenltd  11404  ltaddsub  11734  leord1  11787  lediv1  12130  suprleub  12231  dfinfre  12246  infregelb  12249  nnge1  12291  nnnlt1  12295  avgle1  12503  avgle2  12504  nn0nlt0  12549  recnz  12690  btwnnz  12691  prime  12696  indstr  12955  uzsupss  12979  zbtwnre  12985  rpneg  13064  2resupmax  13226  fzn  13576  nelfzo  13700  fzonlt0  13718  fllt  13842  flflp1  13843  modifeq2int  13970  om2uzlt2i  13988  fsuppmapnn0fiub0  14030  suppssfz  14031  leexp2  14207  discr  14275  bcval4  14342  ccatsymb  14616  swrd0  14692  sqrtneglem  15301  harmonic  15891  efle  16150  dvdsle  16343  dfgcd2  16579  lcmf  16666  infpnlem1  16943  pgpssslw  19646  gsummoncoe1  22327  mp2pm2mplem4  22830  dvferm1  26037  dvferm2  26039  dgrlt  26320  logleb  26659  argrege0  26667  ellogdm  26695  cxple  26751  cxple3  26757  asinneg  26943  birthdaylem3  27010  ppieq0  27233  chpeq0  27266  chteq0  27267  lgsval2lem  27365  lgsneg  27379  lgsdilem  27382  gausslemma2dlem1a  27423  gausslemma2dlem3  27426  ostth2lem1  27676  ostth3  27696  rusgrnumwwlks  30003  clwlkclwwlklem2a  30026  frgrreg  30422  friendship  30427  nmounbi  30804  nmlno0lem  30821  nmlnop0iALT  32023  supfz  35708  inffz  35709  fz0n  35710  nn0prpw  36305  leceifl  37595  poimirlem15  37621  poimirlem16  37622  poimirlem17  37623  poimirlem20  37626  poimirlem24  37630  poimirlem31  37637  poimirlem32  37638  ftc1anclem1  37679  nninfnub  37737  metakunt22  42207  ellz1  42754  rencldnfilem  42807  icccncfext  45842  subsubelfzo0  47275  digexp  48456  reorelicc  48559