Theorem lenlt 11401

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2146   class class class wbr 5106  ℝcr 11212  ℝ^*cxr 11355   < clt 11356   ≤ cle 11357

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-sep 5252  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171  df-xp 5661  df-cnv 5663  df-xr 11360  df-le 11362

This theorem is used by:  ltnle  11402  letri3  11408  leloe  11409  eqlelt  11410  ne0gt0  11428  lelttric  11430  lenlti  11443  lenltd  11469  ltaddsub  11803  leord1  11856  lediv1  12195  suprleub  12296  dfinfre  12311  infregelb  12314  nnge1  12379  nnnlt1  12383  avgle1  12599  avgle2  12600  nn0nlt0  12645  recnz  12787  btwnnz  12788  prime  12793  indstr  13056  uzsupss  13080  zbtwnre  13086  rpneg  13167  2resupmax  13331  fzn  13686  nelfzo  13812  fzonlt0  13830  fllt  13959  flflp1  13960  modifeq2int  14089  om2uzlt2i  14107  fsuppmapnn0fiub0  14149  suppssfz  14150  leexp2  14327  discr  14397  bcval4  14464  ccatsymb  14741  swrd0  14822  sqrtneglem  15448  harmonic  16043  efle  16301  dvdsle  16495  dfgcd2  16734  lcmf  16823  infpnlem1  17103  pgpssslw  19843  gsummoncoe1  22641  mp2pm2mplem4  23142  dvferm1  26320  dvferm2  26322  dgrlt  26600  logleb  26946  argrege0  26954  ellogdm  26982  cxple  27038  cxple3  27044  asinneg  27229  birthdaylem3  27296  ppieq0  27518  chpeq0  27550  chteq0  27551  lgsval2lem  27649  lgsneg  27663  lgsdilem  27666  gausslemma2dlem1a  27707  gausslemma2dlem3  27710  ostth2lem1  27960  ostth3  27980  rusgrnumwwlks  30581  clwlkclwwlklem2a  30604  frgrreg  31010  friendship  31015  nmounbi  31393  nmlno0lem  31410  nmlnop0iALT  32612  supfz  36627  inffz  36628  fz0n  36629  nn0prpw  37244  leceifl  38678  poimirlem15  38699  poimirlem16  38700  poimirlem17  38701  poimirlem20  38704  poimirlem24  38708  poimirlem31  38715  poimirlem32  38716  ftc1anclem1  38757  nninfnub  38831  ellz1  43924  rencldnfilem  43973  icccncfext  47042  subsubelfzo0  48542  digexp  49864  reorelicc  49967