Theorem lenlt 10718

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∈ wcel 2110   class class class wbr 5065  ℝcr 10535  ℝ^*cxr 10673   < clt 10674   ≤ cle 10675

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-nul 5209  ax-pr 5329

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4567  df-pr 4569  df-op 4573  df-br 5066  df-opab 5128  df-xp 5560  df-cnv 5562  df-xr 10678  df-le 10680

This theorem is referenced by:  ltnle  10719  letri3  10725  leloe  10726  eqlelt  10727  ne0gt0  10744  lelttric  10746  lenlti  10759  lenltd  10785  ltaddsub  11113  leord1  11166  lediv1  11504  suprleub  11606  dfinfre  11621  infregelb  11624  nnge1  11664  nnnlt1  11668  avgle1  11876  avgle2  11877  nn0nlt0  11922  recnz  12056  btwnnz  12057  prime  12062  indstr  12315  uzsupss  12339  zbtwnre  12345  rpneg  12420  2resupmax  12580  fzn  12922  nelfzo  13042  fzonlt0  13059  fllt  13175  flflp1  13176  modifeq2int  13300  om2uzlt2i  13318  fsuppmapnn0fiub0  13360  suppssfz  13361  leexp2  13534  discr  13600  bcval4  13666  ccatsymb  13935  swrd0  14019  sqrtneglem  14625  harmonic  15213  efle  15470  dvdsle  15659  dfgcd2  15893  lcmf  15976  infpnlem1  16245  pgpssslw  18738  gsummoncoe1  20471  mp2pm2mplem4  21416  dvferm1  24581  dvferm2  24583  dgrlt  24855  logleb  25185  argrege0  25193  ellogdm  25221  cxple  25277  cxple3  25283  asinneg  25463  birthdaylem3  25530  ppieq0  25752  chpeq0  25783  chteq0  25784  lgsval2lem  25882  lgsneg  25896  lgsdilem  25899  gausslemma2dlem1a  25940  gausslemma2dlem3  25943  ostth2lem1  26193  ostth3  26213  rusgrnumwwlks  27752  clwlkclwwlklem2a  27775  frgrreg  28172  friendship  28177  nmounbi  28552  nmlno0lem  28569  nmlnop0iALT  29771  supfz  32960  inffz  32961  fz0n  32962  nn0prpw  33671  leceifl  34880  poimirlem15  34906  poimirlem16  34907  poimirlem17  34908  poimirlem20  34911  poimirlem24  34915  poimirlem31  34922  poimirlem32  34923  ftc1anclem1  34966  nninfnub  35025  ellz1  39362  rencldnfilem  39415  icccncfext  42168  subsubelfzo0  43525  digexp  44666  reorelicc  44696