Theorem lenlt 11228

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2109   class class class wbr 5102  ℝcr 11043  ℝ^*cxr 11183   < clt 11184   ≤ cle 11185

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-xp 5637  df-cnv 5639  df-xr 11188  df-le 11190

This theorem is referenced by:  ltnle  11229  letri3  11235  leloe  11236  eqlelt  11237  ne0gt0  11255  lelttric  11257  lenlti  11270  lenltd  11296  ltaddsub  11628  leord1  11681  lediv1  12024  suprleub  12125  dfinfre  12140  infregelb  12143  nnge1  12190  nnnlt1  12194  avgle1  12398  avgle2  12399  nn0nlt0  12444  recnz  12585  btwnnz  12586  prime  12591  indstr  12851  uzsupss  12875  zbtwnre  12881  rpneg  12961  2resupmax  13124  fzn  13477  nelfzo  13601  fzonlt0  13619  fllt  13744  flflp1  13745  modifeq2int  13874  om2uzlt2i  13892  fsuppmapnn0fiub0  13934  suppssfz  13935  leexp2  14112  discr  14181  bcval4  14248  ccatsymb  14523  swrd0  14599  sqrtneglem  15208  harmonic  15801  efle  16062  dvdsle  16256  dfgcd2  16492  lcmf  16579  infpnlem1  16857  pgpssslw  19528  gsummoncoe1  22228  mp2pm2mplem4  22729  dvferm1  25922  dvferm2  25924  dgrlt  26205  logleb  26545  argrege0  26553  ellogdm  26581  cxple  26637  cxple3  26643  asinneg  26829  birthdaylem3  26896  ppieq0  27119  chpeq0  27152  chteq0  27153  lgsval2lem  27251  lgsneg  27265  lgsdilem  27268  gausslemma2dlem1a  27309  gausslemma2dlem3  27312  ostth2lem1  27562  ostth3  27582  rusgrnumwwlks  29954  clwlkclwwlklem2a  29977  frgrreg  30373  friendship  30378  nmounbi  30755  nmlno0lem  30772  nmlnop0iALT  31974  supfz  35709  inffz  35710  fz0n  35711  nn0prpw  36304  leceifl  37596  poimirlem15  37622  poimirlem16  37623  poimirlem17  37624  poimirlem20  37627  poimirlem24  37631  poimirlem31  37638  poimirlem32  37639  ftc1anclem1  37680  nninfnub  37738  ellz1  42748  rencldnfilem  42801  icccncfext  45878  subsubelfzo0  47320  digexp  48589  reorelicc  48692