Theorem lenlt 11263

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399   ∈ wcel 2144   class class class wbr 5102  ℝcr 11074  ℝ^*cxr 11217   < clt 11218   ≤ cle 11219

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-sep 5248  ax-pr 5392

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-ral 3079  df-rex 3089  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5103  df-opab 5165  df-xp 5655  df-cnv 5657  df-xr 11222  df-le 11224

This theorem is referenced by:  ltnle  11264  letri3  11270  leloe  11271  eqlelt  11272  ne0gt0  11290  lelttric  11292  lenlti  11305  lenltd  11331  ltaddsub  11663  leord1  11716  lediv1  12059  suprleub  12160  dfinfre  12175  infregelb  12178  nnge1  12243  nnnlt1  12247  avgle1  12463  avgle2  12464  nn0nlt0  12509  recnz  12650  btwnnz  12651  prime  12656  indstr  12919  uzsupss  12943  zbtwnre  12949  rpneg  13029  2resupmax  13193  fzn  13547  nelfzo  13672  fzonlt0  13690  fllt  13818  flflp1  13819  modifeq2int  13948  om2uzlt2i  13966  fsuppmapnn0fiub0  14008  suppssfz  14009  leexp2  14186  discr  14255  bcval4  14322  ccatsymb  14598  swrd0  14674  sqrtneglem  15295  harmonic  15891  efle  16152  dvdsle  16346  dfgcd2  16582  lcmf  16669  infpnlem1  16948  pgpssslw  19656  gsummoncoe1  22373  mp2pm2mplem4  22871  dvferm1  26049  dvferm2  26051  dgrlt  26328  logleb  26670  argrege0  26678  ellogdm  26706  cxple  26762  cxple3  26768  asinneg  26953  birthdaylem3  27020  ppieq0  27242  chpeq0  27274  chteq0  27275  lgsval2lem  27373  lgsneg  27387  lgsdilem  27390  gausslemma2dlem1a  27431  gausslemma2dlem3  27434  ostth2lem1  27684  ostth3  27704  rusgrnumwwlks  30179  clwlkclwwlklem2a  30202  frgrreg  30598  friendship  30603  nmounbi  30981  nmlno0lem  30998  nmlnop0iALT  32200  supfz  36084  inffz  36085  fz0n  36086  nn0prpw  36688  leceifl  38113  poimirlem15  38139  poimirlem16  38140  poimirlem17  38141  poimirlem20  38144  poimirlem24  38148  poimirlem31  38155  poimirlem32  38156  ftc1anclem1  38197  nninfnub  38255  ellz1  43353  rencldnfilem  43402  icccncfext  46466  subsubelfzo0  47926  digexp  49234  reorelicc  49337