Theorem lenlt 10521

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 387   ∈ wcel 2050   class class class wbr 4930  ℝcr 10336  ℝ^*cxr 10475   < clt 10476   ≤ cle 10477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5061  ax-nul 5068  ax-pr 5187

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2583  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3417  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-nul 4181  df-if 4352  df-sn 4443  df-pr 4445  df-op 4449  df-br 4931  df-opab 4993  df-xp 5414  df-cnv 5416  df-xr 10480  df-le 10482

This theorem is referenced by:  ltnle  10522  letri3  10528  leloe  10529  eqlelt  10530  ne0gt0  10547  lelttric  10549  lenlti  10562  lenltd  10588  ltaddsub  10917  leord1  10970  lediv1  11308  suprleub  11410  dfinfre  11425  infregelb  11428  nnge1  11471  nnnlt1  11475  avgle1  11690  avgle2  11691  nn0nlt0  11738  recnz  11873  btwnnz  11874  prime  11879  indstr  12133  uzsupss  12157  zbtwnre  12163  rpneg  12241  2resupmax  12401  fzn  12742  nelfzo  12862  fzonlt0  12878  fllt  12994  flflp1  12995  modifeq2int  13119  om2uzlt2i  13137  fsuppmapnn0fiub0  13179  suppssfz  13180  leexp2  13353  discr  13419  bcval4  13485  ccatsymb  13748  swrd0  13829  sqrtneglem  14490  harmonic  15077  efle  15334  dvdsle  15523  dfgcd2  15753  lcmf  15836  infpnlem1  16105  pgpssslw  18503  gsummoncoe1  20178  mp2pm2mplem4  21124  dvferm1  24288  dvferm2  24290  dgrlt  24562  logleb  24890  argrege0  24898  ellogdm  24926  cxple  24982  cxple3  24988  asinneg  25168  birthdaylem3  25236  ppieq0  25458  chpeq0  25489  chteq0  25490  lgsval2lem  25588  lgsneg  25602  lgsdilem  25605  gausslemma2dlem1a  25646  gausslemma2dlem3  25649  ostth2lem1  25899  ostth3  25919  rusgrnumwwlks  27483  rusgrnumwwlksOLD  27484  clwlkclwwlklem2a  27507  frgrreg  27954  friendship  27959  nmounbi  28333  nmlno0lem  28350  nmlnop0iALT  29556  supfz  32480  inffz  32481  fz0n  32482  nn0prpw  33192  leceifl  34322  poimirlem15  34348  poimirlem16  34349  poimirlem17  34350  poimirlem20  34353  poimirlem24  34357  poimirlem31  34364  poimirlem32  34365  ftc1anclem1  34408  nninfnub  34468  ellz1  38759  rencldnfilem  38813  limsup10ex  41486  icccncfext  41601  subsubelfzo0  42933  digexp  44036  reorelicc  44066