Theorem lenlt 11292

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∈ wcel 2143   class class class wbr 5109  ℝcr 11103  ℝ^*cxr 11246   < clt 11247   ≤ cle 11248

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-xp 5667  df-cnv 5669  df-xr 11251  df-le 11253

This theorem is used by:  ltnle  11293  letri3  11299  leloe  11300  eqlelt  11301  ne0gt0  11319  lelttric  11321  lenlti  11334  lenltd  11360  ltaddsub  11692  leord1  11745  lediv1  12084  suprleub  12185  dfinfre  12200  infregelb  12203  nnge1  12268  nnnlt1  12272  avgle1  12488  avgle2  12489  nn0nlt0  12534  recnz  12675  btwnnz  12676  prime  12681  indstr  12944  uzsupss  12968  zbtwnre  12974  rpneg  13054  2resupmax  13218  fzn  13572  nelfzo  13698  fzonlt0  13716  fllt  13844  flflp1  13845  modifeq2int  13974  om2uzlt2i  13992  fsuppmapnn0fiub0  14034  suppssfz  14035  leexp2  14212  discr  14281  bcval4  14348  ccatsymb  14625  swrd0  14701  sqrtneglem  15322  harmonic  15918  efle  16178  dvdsle  16372  dfgcd2  16608  lcmf  16695  infpnlem1  16974  pgpssslw  19688  gsummoncoe1  22477  mp2pm2mplem4  22975  dvferm1  26153  dvferm2  26155  dgrlt  26432  logleb  26777  argrege0  26785  ellogdm  26813  cxple  26869  cxple3  26875  asinneg  27060  birthdaylem3  27127  ppieq0  27349  chpeq0  27381  chteq0  27382  lgsval2lem  27480  lgsneg  27494  lgsdilem  27497  gausslemma2dlem1a  27538  gausslemma2dlem3  27541  ostth2lem1  27791  ostth3  27811  rusgrnumwwlks  30335  clwlkclwwlklem2a  30358  frgrreg  30754  friendship  30759  nmounbi  31137  nmlno0lem  31154  nmlnop0iALT  32356  supfz  36229  inffz  36230  fz0n  36231  nn0prpw  36862  leceifl  38288  poimirlem15  38314  poimirlem16  38315  poimirlem17  38316  poimirlem20  38319  poimirlem24  38323  poimirlem31  38330  poimirlem32  38331  ftc1anclem1  38372  nninfnub  38430  ellz1  43526  rencldnfilem  43575  icccncfext  46629  subsubelfzo0  48092  digexp  49415  reorelicc  49518