Theorem lenlt 11330

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 394   ∈ wcel 2098   class class class wbr 5152  ℝcr 11145  ℝ^*cxr 11285   < clt 11286   ≤ cle 11287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pr 5433

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-ral 3059  df-rex 3068  df-rab 3431  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-br 5153  df-opab 5215  df-xp 5688  df-cnv 5690  df-xr 11290  df-le 11292

This theorem is referenced by:  ltnle  11331  letri3  11337  leloe  11338  eqlelt  11339  ne0gt0  11357  lelttric  11359  lenlti  11372  lenltd  11398  ltaddsub  11726  leord1  11779  lediv1  12117  suprleub  12218  dfinfre  12233  infregelb  12236  nnge1  12278  nnnlt1  12282  avgle1  12490  avgle2  12491  nn0nlt0  12536  recnz  12675  btwnnz  12676  prime  12681  indstr  12938  uzsupss  12962  zbtwnre  12968  rpneg  13046  2resupmax  13207  fzn  13557  nelfzo  13677  fzonlt0  13695  fllt  13811  flflp1  13812  modifeq2int  13938  om2uzlt2i  13956  fsuppmapnn0fiub0  13998  suppssfz  13999  leexp2  14175  discr  14242  bcval4  14306  ccatsymb  14572  swrd0  14648  sqrtneglem  15253  harmonic  15845  efle  16102  dvdsle  16294  dfgcd2  16529  lcmf  16611  infpnlem1  16886  pgpssslw  19576  gsummoncoe1  22234  mp2pm2mplem4  22731  dvferm1  25937  dvferm2  25939  dgrlt  26221  logleb  26557  argrege0  26565  ellogdm  26593  cxple  26649  cxple3  26655  asinneg  26838  birthdaylem3  26905  ppieq0  27128  chpeq0  27161  chteq0  27162  lgsval2lem  27260  lgsneg  27274  lgsdilem  27277  gausslemma2dlem1a  27318  gausslemma2dlem3  27321  ostth2lem1  27571  ostth3  27591  rusgrnumwwlks  29805  clwlkclwwlklem2a  29828  frgrreg  30224  friendship  30229  nmounbi  30606  nmlno0lem  30623  nmlnop0iALT  31825  supfz  35356  inffz  35357  fz0n  35358  nn0prpw  35840  leceifl  37115  poimirlem15  37141  poimirlem16  37142  poimirlem17  37143  poimirlem20  37146  poimirlem24  37150  poimirlem31  37157  poimirlem32  37158  ftc1anclem1  37199  nninfnub  37257  metakunt22  41710  ellz1  42218  rencldnfilem  42271  icccncfext  45304  subsubelfzo0  46735  digexp  47758  reorelicc  47861