Theorem lenlt 11368

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2108   class class class wbr 5166  ℝcr 11183  ℝ^*cxr 11323   < clt 11324   ≤ cle 11325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-xp 5706  df-cnv 5708  df-xr 11328  df-le 11330

This theorem is referenced by:  ltnle  11369  letri3  11375  leloe  11376  eqlelt  11377  ne0gt0  11395  lelttric  11397  lenlti  11410  lenltd  11436  ltaddsub  11764  leord1  11817  lediv1  12160  suprleub  12261  dfinfre  12276  infregelb  12279  nnge1  12321  nnnlt1  12325  avgle1  12533  avgle2  12534  nn0nlt0  12579  recnz  12718  btwnnz  12719  prime  12724  indstr  12981  uzsupss  13005  zbtwnre  13011  rpneg  13089  2resupmax  13250  fzn  13600  nelfzo  13721  fzonlt0  13739  fllt  13857  flflp1  13858  modifeq2int  13984  om2uzlt2i  14002  fsuppmapnn0fiub0  14044  suppssfz  14045  leexp2  14221  discr  14289  bcval4  14356  ccatsymb  14630  swrd0  14706  sqrtneglem  15315  harmonic  15907  efle  16166  dvdsle  16358  dfgcd2  16593  lcmf  16680  infpnlem1  16957  pgpssslw  19656  gsummoncoe1  22333  mp2pm2mplem4  22836  dvferm1  26043  dvferm2  26045  dgrlt  26326  logleb  26663  argrege0  26671  ellogdm  26699  cxple  26755  cxple3  26761  asinneg  26947  birthdaylem3  27014  ppieq0  27237  chpeq0  27270  chteq0  27271  lgsval2lem  27369  lgsneg  27383  lgsdilem  27386  gausslemma2dlem1a  27427  gausslemma2dlem3  27430  ostth2lem1  27680  ostth3  27700  rusgrnumwwlks  30007  clwlkclwwlklem2a  30030  frgrreg  30426  friendship  30431  nmounbi  30808  nmlno0lem  30825  nmlnop0iALT  32027  supfz  35691  inffz  35692  fz0n  35693  nn0prpw  36289  leceifl  37569  poimirlem15  37595  poimirlem16  37596  poimirlem17  37597  poimirlem20  37600  poimirlem24  37604  poimirlem31  37611  poimirlem32  37612  ftc1anclem1  37653  nninfnub  37711  metakunt22  42183  ellz1  42723  rencldnfilem  42776  icccncfext  45808  subsubelfzo0  47241  digexp  48341  reorelicc  48444