Theorem lenlt 11252

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2109   class class class wbr 5107  ℝcr 11067  ℝ^*cxr 11207   < clt 11208   ≤ cle 11209

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 5251  ax-nul 5261  ax-pr 5387

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644  df-cnv 5646  df-xr 11212  df-le 11214

This theorem is referenced by:  ltnle  11253  letri3  11259  leloe  11260  eqlelt  11261  ne0gt0  11279  lelttric  11281  lenlti  11294  lenltd  11320  ltaddsub  11652  leord1  11705  lediv1  12048  suprleub  12149  dfinfre  12164  infregelb  12167  nnge1  12214  nnnlt1  12218  avgle1  12422  avgle2  12423  nn0nlt0  12468  recnz  12609  btwnnz  12610  prime  12615  indstr  12875  uzsupss  12899  zbtwnre  12905  rpneg  12985  2resupmax  13148  fzn  13501  nelfzo  13625  fzonlt0  13643  fllt  13768  flflp1  13769  modifeq2int  13898  om2uzlt2i  13916  fsuppmapnn0fiub0  13958  suppssfz  13959  leexp2  14136  discr  14205  bcval4  14272  ccatsymb  14547  swrd0  14623  sqrtneglem  15232  harmonic  15825  efle  16086  dvdsle  16280  dfgcd2  16516  lcmf  16603  infpnlem1  16881  pgpssslw  19544  gsummoncoe1  22195  mp2pm2mplem4  22696  dvferm1  25889  dvferm2  25891  dgrlt  26172  logleb  26512  argrege0  26520  ellogdm  26548  cxple  26604  cxple3  26610  asinneg  26796  birthdaylem3  26863  ppieq0  27086  chpeq0  27119  chteq0  27120  lgsval2lem  27218  lgsneg  27232  lgsdilem  27235  gausslemma2dlem1a  27276  gausslemma2dlem3  27279  ostth2lem1  27529  ostth3  27549  rusgrnumwwlks  29904  clwlkclwwlklem2a  29927  frgrreg  30323  friendship  30328  nmounbi  30705  nmlno0lem  30722  nmlnop0iALT  31924  supfz  35716  inffz  35717  fz0n  35718  nn0prpw  36311  leceifl  37603  poimirlem15  37629  poimirlem16  37630  poimirlem17  37631  poimirlem20  37634  poimirlem24  37638  poimirlem31  37645  poimirlem32  37646  ftc1anclem1  37687  nninfnub  37745  ellz1  42755  rencldnfilem  42808  icccncfext  45885  subsubelfzo0  47327  digexp  48596  reorelicc  48699