Theorem lenlt 11099

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397   ∈ wcel 2104   class class class wbr 5081  ℝcr 10916  ℝ^*cxr 11054   < clt 11055   ≤ cle 11056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pr 5361

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3063  df-rex 3072  df-rab 3287  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-br 5082  df-opab 5144  df-xp 5606  df-cnv 5608  df-xr 11059  df-le 11061

This theorem is referenced by:  ltnle  11100  letri3  11106  leloe  11107  eqlelt  11108  ne0gt0  11126  lelttric  11128  lenlti  11141  lenltd  11167  ltaddsub  11495  leord1  11548  lediv1  11886  suprleub  11987  dfinfre  12002  infregelb  12005  nnge1  12047  nnnlt1  12051  avgle1  12259  avgle2  12260  nn0nlt0  12305  recnz  12441  btwnnz  12442  prime  12447  indstr  12702  uzsupss  12726  zbtwnre  12732  rpneg  12808  2resupmax  12968  fzn  13318  nelfzo  13438  fzonlt0  13456  fllt  13572  flflp1  13573  modifeq2int  13699  om2uzlt2i  13717  fsuppmapnn0fiub0  13759  suppssfz  13760  leexp2  13935  discr  14001  bcval4  14067  ccatsymb  14332  swrd0  14416  sqrtneglem  15023  harmonic  15616  efle  15872  dvdsle  16064  dfgcd2  16299  lcmf  16383  infpnlem1  16656  pgpssslw  19264  gsummoncoe1  21520  mp2pm2mplem4  22003  dvferm1  25194  dvferm2  25196  dgrlt  25472  logleb  25803  argrege0  25811  ellogdm  25839  cxple  25895  cxple3  25901  asinneg  26081  birthdaylem3  26148  ppieq0  26370  chpeq0  26401  chteq0  26402  lgsval2lem  26500  lgsneg  26514  lgsdilem  26517  gausslemma2dlem1a  26558  gausslemma2dlem3  26561  ostth2lem1  26811  ostth3  26831  rusgrnumwwlks  28384  clwlkclwwlklem2a  28407  frgrreg  28803  friendship  28808  nmounbi  29183  nmlno0lem  29200  nmlnop0iALT  30402  supfz  33739  inffz  33740  fz0n  33741  nn0prpw  34557  leceifl  35810  poimirlem15  35836  poimirlem16  35837  poimirlem17  35838  poimirlem20  35841  poimirlem24  35845  poimirlem31  35852  poimirlem32  35853  ftc1anclem1  35894  nninfnub  35953  metakunt22  40188  ellz1  40626  rencldnfilem  40679  icccncfext  43477  subsubelfzo0  44876  digexp  46011  reorelicc  46114