Theorem lenlt 11212

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2114   class class class wbr 5086  ℝcr 11026  ℝ^*cxr 11166   < clt 11167   ≤ cle 11168

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 5231  ax-pr 5368

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 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-xp 5628  df-cnv 5630  df-xr 11171  df-le 11173

This theorem is referenced by:  ltnle  11213  letri3  11219  leloe  11220  eqlelt  11221  ne0gt0  11239  lelttric  11241  lenlti  11254  lenltd  11280  ltaddsub  11612  leord1  11665  lediv1  12008  suprleub  12109  dfinfre  12124  infregelb  12127  nnge1  12174  nnnlt1  12178  avgle1  12382  avgle2  12383  nn0nlt0  12428  recnz  12568  btwnnz  12569  prime  12574  indstr  12830  uzsupss  12854  zbtwnre  12860  rpneg  12940  2resupmax  13104  fzn  13457  nelfzo  13581  fzonlt0  13599  fllt  13727  flflp1  13728  modifeq2int  13857  om2uzlt2i  13875  fsuppmapnn0fiub0  13917  suppssfz  13918  leexp2  14095  discr  14164  bcval4  14231  ccatsymb  14507  swrd0  14583  sqrtneglem  15190  harmonic  15783  efle  16044  dvdsle  16238  dfgcd2  16474  lcmf  16561  infpnlem1  16839  pgpssslw  19547  gsummoncoe1  22251  mp2pm2mplem4  22752  dvferm1  25930  dvferm2  25932  dgrlt  26212  logleb  26552  argrege0  26560  ellogdm  26588  cxple  26644  cxple3  26650  asinneg  26836  birthdaylem3  26903  ppieq0  27126  chpeq0  27159  chteq0  27160  lgsval2lem  27258  lgsneg  27272  lgsdilem  27275  gausslemma2dlem1a  27316  gausslemma2dlem3  27319  ostth2lem1  27569  ostth3  27589  rusgrnumwwlks  30034  clwlkclwwlklem2a  30057  frgrreg  30453  friendship  30458  nmounbi  30836  nmlno0lem  30853  nmlnop0iALT  32055  supfz  35917  inffz  35918  fz0n  35919  nn0prpw  36511  leceifl  37921  poimirlem15  37947  poimirlem16  37948  poimirlem17  37949  poimirlem20  37952  poimirlem24  37956  poimirlem31  37963  poimirlem32  37964  ftc1anclem1  38005  nninfnub  38063  ellz1  43198  rencldnfilem  43251  icccncfext  46319  subsubelfzo0  47760  digexp  49041  reorelicc  49144