---

Step * of Lemma rmul-minus

No Annotations
∀[r:ℝ]. ∀[n:ℤ].  ((r * r(-n)) = (-(r) * r(n)))
BY
{ (Auto⋅
   THEN RWO "rminus-as-rmul" 0
   THEN Auto
   THEN RWO "rmul_comm" 0
   THEN Auto
   THEN RWO "rmul-assoc" 0
   THEN Auto
   THEN BLemma `rmul_functionality`
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[r:\mBbbR{}].  \mforall{}[n:\mBbbZ{}].    ((r  *  r(-n))  =  (-(r)  *  r(n)))


By

---

Latex:
(Auto\mcdot{}
  THEN  RWO  "rminus-as-rmul"  0
  THEN  Auto
  THEN  RWO  "rmul\_comm"  0
  THEN  Auto
  THEN  RWO  "rmul-assoc"  0
  THEN  Auto
  THEN  BLemma  `rmul\_functionality`
  THEN  Auto)

---

Home Index