---

Step * of Lemma qmul_over_minus_qrng

No Annotations
∀[a,b:ℚ].  (((-(a) * b) = -(a * b) ∈ ℚ) ∧ ((a * -(b)) = -(a * b) ∈ ℚ))
BY
{ (ProveSpecializedLemmaWReduce rng_times_over_minus) 0 [⌜parm{i}⌝;⌜<ℚ+*>⌝]⋅ }

---

Latex:

---

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


By

---

Latex:
(ProveSpecializedLemmaWReduce  rng\_times\_over\_minus)  0  [\mkleeneopen{}parm\{i\}\mkleeneclose{};\mkleeneopen{}<\mBbbQ{}+*>\mkleeneclose{}]\mcdot{}

---

Home Index