Theorem lenlt 10876

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∈ wcel 2112   class class class wbr 5039  ℝcr 10693  ℝ^*cxr 10831   < clt 10832   ≤ cle 10833

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-br 5040  df-opab 5102  df-xp 5542  df-cnv 5544  df-xr 10836  df-le 10838

This theorem is referenced by:  ltnle  10877  letri3  10883  leloe  10884  eqlelt  10885  ne0gt0  10902  lelttric  10904  lenlti  10917  lenltd  10943  ltaddsub  11271  leord1  11324  lediv1  11662  suprleub  11763  dfinfre  11778  infregelb  11781  nnge1  11823  nnnlt1  11827  avgle1  12035  avgle2  12036  nn0nlt0  12081  recnz  12217  btwnnz  12218  prime  12223  indstr  12477  uzsupss  12501  zbtwnre  12507  rpneg  12583  2resupmax  12743  fzn  13093  nelfzo  13213  fzonlt0  13230  fllt  13346  flflp1  13347  modifeq2int  13471  om2uzlt2i  13489  fsuppmapnn0fiub0  13531  suppssfz  13532  leexp2  13706  discr  13772  bcval4  13838  ccatsymb  14104  swrd0  14188  sqrtneglem  14795  harmonic  15386  efle  15642  dvdsle  15834  dfgcd2  16069  lcmf  16153  infpnlem1  16426  pgpssslw  18957  gsummoncoe1  21179  mp2pm2mplem4  21660  dvferm1  24836  dvferm2  24838  dgrlt  25114  logleb  25445  argrege0  25453  ellogdm  25481  cxple  25537  cxple3  25543  asinneg  25723  birthdaylem3  25790  ppieq0  26012  chpeq0  26043  chteq0  26044  lgsval2lem  26142  lgsneg  26156  lgsdilem  26159  gausslemma2dlem1a  26200  gausslemma2dlem3  26203  ostth2lem1  26453  ostth3  26473  rusgrnumwwlks  28012  clwlkclwwlklem2a  28035  frgrreg  28431  friendship  28436  nmounbi  28811  nmlno0lem  28828  nmlnop0iALT  30030  supfz  33363  inffz  33364  fz0n  33365  nn0prpw  34198  leceifl  35452  poimirlem15  35478  poimirlem16  35479  poimirlem17  35480  poimirlem20  35483  poimirlem24  35487  poimirlem31  35494  poimirlem32  35495  ftc1anclem1  35536  nninfnub  35595  metakunt22  39809  ellz1  40233  rencldnfilem  40286  icccncfext  43046  subsubelfzo0  44434  digexp  45569  reorelicc  45672