---

Step * of Lemma rmul_over_rminus

No Annotations
∀[a,b:ℝ].  (((-(a) * b) = -(a * b)) ∧ ((a * -(b)) = -(a * b)))
BY
{ ((Assert ∀a,b:ℝ.  ((-(a) * b) = -(a * b)) BY
          (Auto THEN RWO "rminus-as-rmul rmul-assoc" 0⋅ THEN Auto))
   THEN Auto
   THEN (InstHyp [⌜b⌝; ⌜a⌝] 1)⋅
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[a,b:\mBbbR{}].    (((-(a)  *  b)  =  -(a  *  b))  \mwedge{}  ((a  *  -(b))  =  -(a  *  b)))


By

---

Latex:
((Assert  \mforall{}a,b:\mBbbR{}.    ((-(a)  *  b)  =  -(a  *  b))  BY
                (Auto  THEN  RWO  "rminus-as-rmul  rmul-assoc"  0\mcdot{}  THEN  Auto))
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}b\mkleeneclose{};  \mkleeneopen{}a\mkleeneclose{}]  1)\mcdot{}
  THEN  Auto)

---

Home Index