MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ltnle Structured version   Visualization version   GIF version

Theorem ltnle 10069
Description: 'Less than' expressed in terms of 'less than or equal to'. (Contributed by NM, 11-Jul-2005.)
Assertion
Ref Expression
ltnle ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ 𝐵𝐴))

Proof of Theorem ltnle
StepHypRef Expression
1 lenlt 10068 . . 3 ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵𝐴 ↔ ¬ 𝐴 < 𝐵))
21ancoms 469 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵𝐴 ↔ ¬ 𝐴 < 𝐵))
32con2bid 344 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ 𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  wcel 1987   class class class wbr 4618  cr 9887   < clt 10026  cle 10027
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pr 4872
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-br 4619  df-opab 4679  df-xp 5085  df-cnv 5087  df-xr 10030  df-le 10032
This theorem is referenced by:  letric  10089  ltnled  10136  leaddsub  10456  mulge0b  10845  nnnle0  11003  nn0n0n1ge2b  11311  znnnlt1  11356  uzwo  11703  qsqueeze  11983  difreicc  12254  fzp1disj  12349  fzneuz  12370  fznuz  12371  uznfz  12372  difelfznle  12402  nelfzo  12424  ssfzoulel  12511  elfzonelfzo  12519  modfzo0difsn  12690  ssnn0fi  12732  discr1  12948  facdiv  13022  bcval5  13053  ccatsymb  13313  swrdnd  13378  swrdsbslen  13394  swrdspsleq  13395  swrdccat3  13437  repswswrd  13476  cnpart  13922  absmax  14011  rlimrege0  14252  znnenlem  14876  rpnnen2lem12  14890  alzdvds  14977  algcvgblem  15225  prmndvdsfaclt  15370  pcprendvds  15480  pcdvdsb  15508  pcmpt  15531  prmunb  15553  prmreclem2  15556  prmgaplem5  15694  prmgaplem6  15695  prmlem1  15749  prmlem2  15762  lt6abl  18228  metdseq0  22580  xrhmeo  22668  ovolicc2lem3  23210  itg2seq  23432  dvne0  23695  coeeulem  23901  radcnvlt1  24093  argimgt0  24279  cxple2  24360  ressatans  24578  eldmgm  24665  basellem2  24725  issqf  24779  bpos1  24925  bposlem3  24928  bposlem6  24931  pntpbnd2  25193  ostth2lem4  25242  crctcshwlkn0  26599  crctcsh  26602  eucrctshift  26986  ltflcei  33064  poimirlem4  33080  poimirlem13  33089  poimirlem14  33090  poimirlem15  33091  poimirlem31  33107  mblfinlem1  33113  mbfposadd  33124  itgaddnclem2  33136  ftc1anclem1  33152  ftc1anclem5  33156  dvasin  33163  icccncfext  39431  stoweidlem14  39564  stoweidlem34  39584  ltnltne  40636  pfxccat3  40751  pfxccat3a  40754  nnsum4primeseven  41003  nnsum4primesevenALTV  41004  ply1mulgsumlem2  41489
  Copyright terms: Public domain W3C validator