Theorem lenlt 11292

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397   ∈ wcel 2107   class class class wbr 5149  ℝcr 11109  ℝ^*cxr 11247   < clt 11248   ≤ cle 11249

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 5300  ax-nul 5307  ax-pr 5428

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 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-xp 5683  df-cnv 5685  df-xr 11252  df-le 11254

This theorem is referenced by:  ltnle  11293  letri3  11299  leloe  11300  eqlelt  11301  ne0gt0  11319  lelttric  11321  lenlti  11334  lenltd  11360  ltaddsub  11688  leord1  11741  lediv1  12079  suprleub  12180  dfinfre  12195  infregelb  12198  nnge1  12240  nnnlt1  12244  avgle1  12452  avgle2  12453  nn0nlt0  12498  recnz  12637  btwnnz  12638  prime  12643  indstr  12900  uzsupss  12924  zbtwnre  12930  rpneg  13006  2resupmax  13167  fzn  13517  nelfzo  13637  fzonlt0  13655  fllt  13771  flflp1  13772  modifeq2int  13898  om2uzlt2i  13916  fsuppmapnn0fiub0  13958  suppssfz  13959  leexp2  14136  discr  14203  bcval4  14267  ccatsymb  14532  swrd0  14608  sqrtneglem  15213  harmonic  15805  efle  16061  dvdsle  16253  dfgcd2  16488  lcmf  16570  infpnlem1  16843  pgpssslw  19482  gsummoncoe1  21828  mp2pm2mplem4  22311  dvferm1  25502  dvferm2  25504  dgrlt  25780  logleb  26111  argrege0  26119  ellogdm  26147  cxple  26203  cxple3  26209  asinneg  26391  birthdaylem3  26458  ppieq0  26680  chpeq0  26711  chteq0  26712  lgsval2lem  26810  lgsneg  26824  lgsdilem  26827  gausslemma2dlem1a  26868  gausslemma2dlem3  26871  ostth2lem1  27121  ostth3  27141  rusgrnumwwlks  29228  clwlkclwwlklem2a  29251  frgrreg  29647  friendship  29652  nmounbi  30029  nmlno0lem  30046  nmlnop0iALT  31248  supfz  34698  inffz  34699  fz0n  34700  nn0prpw  35208  leceifl  36477  poimirlem15  36503  poimirlem16  36504  poimirlem17  36505  poimirlem20  36508  poimirlem24  36512  poimirlem31  36519  poimirlem32  36520  ftc1anclem1  36561  nninfnub  36619  metakunt22  41006  ellz1  41505  rencldnfilem  41558  icccncfext  44603  subsubelfzo0  46034  digexp  47293  reorelicc  47396