Theorem lenlt 11215

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2114   class class class wbr 5099  ℝcr 11029  ℝ^*cxr 11169   < clt 11170   ≤ cle 11171

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-xp 5631  df-cnv 5633  df-xr 11174  df-le 11176

This theorem is referenced by:  ltnle  11216  letri3  11222  leloe  11223  eqlelt  11224  ne0gt0  11242  lelttric  11244  lenlti  11257  lenltd  11283  ltaddsub  11615  leord1  11668  lediv1  12011  suprleub  12112  dfinfre  12127  infregelb  12130  nnge1  12177  nnnlt1  12181  avgle1  12385  avgle2  12386  nn0nlt0  12431  recnz  12571  btwnnz  12572  prime  12577  indstr  12833  uzsupss  12857  zbtwnre  12863  rpneg  12943  2resupmax  13107  fzn  13460  nelfzo  13584  fzonlt0  13602  fllt  13730  flflp1  13731  modifeq2int  13860  om2uzlt2i  13878  fsuppmapnn0fiub0  13920  suppssfz  13921  leexp2  14098  discr  14167  bcval4  14234  ccatsymb  14510  swrd0  14586  sqrtneglem  15193  harmonic  15786  efle  16047  dvdsle  16241  dfgcd2  16477  lcmf  16564  infpnlem1  16842  pgpssslw  19547  gsummoncoe1  22256  mp2pm2mplem4  22757  dvferm1  25949  dvferm2  25951  dgrlt  26232  logleb  26572  argrege0  26580  ellogdm  26608  cxple  26664  cxple3  26670  asinneg  26856  birthdaylem3  26923  ppieq0  27146  chpeq0  27179  chteq0  27180  lgsval2lem  27278  lgsneg  27292  lgsdilem  27295  gausslemma2dlem1a  27336  gausslemma2dlem3  27339  ostth2lem1  27589  ostth3  27609  rusgrnumwwlks  30054  clwlkclwwlklem2a  30077  frgrreg  30473  friendship  30478  nmounbi  30855  nmlno0lem  30872  nmlnop0iALT  32074  supfz  35925  inffz  35926  fz0n  35927  nn0prpw  36519  leceifl  37812  poimirlem15  37838  poimirlem16  37839  poimirlem17  37840  poimirlem20  37843  poimirlem24  37847  poimirlem31  37854  poimirlem32  37855  ftc1anclem1  37896  nninfnub  37954  ellz1  43076  rencldnfilem  43129  icccncfext  46198  subsubelfzo0  47639  digexp  48920  reorelicc  49023