---

Step * of Lemma qmul_over_plus_qrng

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

---

Latex:

---

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


By

---

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

---

Home Index