Theorem lenlt 11224

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2114   class class class wbr 5085  ℝcr 11037  ℝ^*cxr 11178   < clt 11179   ≤ cle 11180

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 2708  ax-sep 5231  ax-pr 5375

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 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-xp 5637  df-cnv 5639  df-xr 11183  df-le 11185

This theorem is referenced by:  ltnle  11225  letri3  11231  leloe  11232  eqlelt  11233  ne0gt0  11251  lelttric  11253  lenlti  11266  lenltd  11292  ltaddsub  11624  leord1  11677  lediv1  12021  suprleub  12122  dfinfre  12137  infregelb  12140  nnge1  12205  nnnlt1  12209  avgle1  12417  avgle2  12418  nn0nlt0  12463  recnz  12604  btwnnz  12605  prime  12610  indstr  12866  uzsupss  12890  zbtwnre  12896  rpneg  12976  2resupmax  13140  fzn  13494  nelfzo  13619  fzonlt0  13637  fllt  13765  flflp1  13766  modifeq2int  13895  om2uzlt2i  13913  fsuppmapnn0fiub0  13955  suppssfz  13956  leexp2  14133  discr  14202  bcval4  14269  ccatsymb  14545  swrd0  14621  sqrtneglem  15228  harmonic  15824  efle  16085  dvdsle  16279  dfgcd2  16515  lcmf  16602  infpnlem1  16881  pgpssslw  19589  gsummoncoe1  22273  mp2pm2mplem4  22774  dvferm1  25952  dvferm2  25954  dgrlt  26231  logleb  26567  argrege0  26575  ellogdm  26603  cxple  26659  cxple3  26665  asinneg  26850  birthdaylem3  26917  ppieq0  27139  chpeq0  27171  chteq0  27172  lgsval2lem  27270  lgsneg  27284  lgsdilem  27287  gausslemma2dlem1a  27328  gausslemma2dlem3  27331  ostth2lem1  27581  ostth3  27601  rusgrnumwwlks  30045  clwlkclwwlklem2a  30068  frgrreg  30464  friendship  30469  nmounbi  30847  nmlno0lem  30864  nmlnop0iALT  32066  supfz  35911  inffz  35912  fz0n  35913  nn0prpw  36505  leceifl  37930  poimirlem15  37956  poimirlem16  37957  poimirlem17  37958  poimirlem20  37961  poimirlem24  37965  poimirlem31  37972  poimirlem32  37973  ftc1anclem1  38014  nninfnub  38072  ellz1  43199  rencldnfilem  43248  icccncfext  46315  subsubelfzo0  47775  digexp  49083  reorelicc  49186