Theorem lenlt 11037

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∈ wcel 2109   class class class wbr 5078  ℝcr 10854  ℝ^*cxr 10992   < clt 10993   ≤ cle 10994

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-br 5079  df-opab 5141  df-xp 5594  df-cnv 5596  df-xr 10997  df-le 10999

This theorem is referenced by:  ltnle  11038  letri3  11044  leloe  11045  eqlelt  11046  ne0gt0  11063  lelttric  11065  lenlti  11078  lenltd  11104  ltaddsub  11432  leord1  11485  lediv1  11823  suprleub  11924  dfinfre  11939  infregelb  11942  nnge1  11984  nnnlt1  11988  avgle1  12196  avgle2  12197  nn0nlt0  12242  recnz  12378  btwnnz  12379  prime  12384  indstr  12638  uzsupss  12662  zbtwnre  12668  rpneg  12744  2resupmax  12904  fzn  13254  nelfzo  13374  fzonlt0  13391  fllt  13507  flflp1  13508  modifeq2int  13634  om2uzlt2i  13652  fsuppmapnn0fiub0  13694  suppssfz  13695  leexp2  13870  discr  13936  bcval4  14002  ccatsymb  14268  swrd0  14352  sqrtneglem  14959  harmonic  15552  efle  15808  dvdsle  16000  dfgcd2  16235  lcmf  16319  infpnlem1  16592  pgpssslw  19200  gsummoncoe1  21456  mp2pm2mplem4  21939  dvferm1  25130  dvferm2  25132  dgrlt  25408  logleb  25739  argrege0  25747  ellogdm  25775  cxple  25831  cxple3  25837  asinneg  26017  birthdaylem3  26084  ppieq0  26306  chpeq0  26337  chteq0  26338  lgsval2lem  26436  lgsneg  26450  lgsdilem  26453  gausslemma2dlem1a  26494  gausslemma2dlem3  26497  ostth2lem1  26747  ostth3  26767  rusgrnumwwlks  28318  clwlkclwwlklem2a  28341  frgrreg  28737  friendship  28742  nmounbi  29117  nmlno0lem  29134  nmlnop0iALT  30336  supfz  33673  inffz  33674  fz0n  33675  nn0prpw  34491  leceifl  35745  poimirlem15  35771  poimirlem16  35772  poimirlem17  35773  poimirlem20  35776  poimirlem24  35780  poimirlem31  35787  poimirlem32  35788  ftc1anclem1  35829  nninfnub  35888  metakunt22  40126  ellz1  40569  rencldnfilem  40622  icccncfext  43382  subsubelfzo0  44770  digexp  45905  reorelicc  46008