Theorem lenlt 11289

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397   ∈ wcel 2107   class class class wbr 5148  ℝcr 11106  ℝ^*cxr 11244   < clt 11245   ≤ cle 11246

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-xp 5682  df-cnv 5684  df-xr 11249  df-le 11251

This theorem is referenced by:  ltnle  11290  letri3  11296  leloe  11297  eqlelt  11298  ne0gt0  11316  lelttric  11318  lenlti  11331  lenltd  11357  ltaddsub  11685  leord1  11738  lediv1  12076  suprleub  12177  dfinfre  12192  infregelb  12195  nnge1  12237  nnnlt1  12241  avgle1  12449  avgle2  12450  nn0nlt0  12495  recnz  12634  btwnnz  12635  prime  12640  indstr  12897  uzsupss  12921  zbtwnre  12927  rpneg  13003  2resupmax  13164  fzn  13514  nelfzo  13634  fzonlt0  13652  fllt  13768  flflp1  13769  modifeq2int  13895  om2uzlt2i  13913  fsuppmapnn0fiub0  13955  suppssfz  13956  leexp2  14133  discr  14200  bcval4  14264  ccatsymb  14529  swrd0  14605  sqrtneglem  15210  harmonic  15802  efle  16058  dvdsle  16250  dfgcd2  16485  lcmf  16567  infpnlem1  16840  pgpssslw  19477  gsummoncoe1  21820  mp2pm2mplem4  22303  dvferm1  25494  dvferm2  25496  dgrlt  25772  logleb  26103  argrege0  26111  ellogdm  26139  cxple  26195  cxple3  26201  asinneg  26381  birthdaylem3  26448  ppieq0  26670  chpeq0  26701  chteq0  26702  lgsval2lem  26800  lgsneg  26814  lgsdilem  26817  gausslemma2dlem1a  26858  gausslemma2dlem3  26861  ostth2lem1  27111  ostth3  27131  rusgrnumwwlks  29218  clwlkclwwlklem2a  29241  frgrreg  29637  friendship  29642  nmounbi  30017  nmlno0lem  30034  nmlnop0iALT  31236  supfz  34687  inffz  34688  fz0n  34689  nn0prpw  35197  leceifl  36466  poimirlem15  36492  poimirlem16  36493  poimirlem17  36494  poimirlem20  36497  poimirlem24  36501  poimirlem31  36508  poimirlem32  36509  ftc1anclem1  36550  nninfnub  36608  metakunt22  40995  ellz1  41491  rencldnfilem  41544  icccncfext  44590  subsubelfzo0  46021  digexp  47247  reorelicc  47350