---

Step * of Lemma qabs-qmul-case2

∀[r,s,a:ℚ].  (|(a * r) - a * s| = (|r - s| * |a|) ∈ ℚ)
BY
{ xxx(Auto THEN (Subst' ((a * r) - a * s) = ((r - s) * a) ∈ ℚ 0 THENA Auto))xxx }

---

Latex:

---

Latex:
\mforall{}[r,s,a:\mBbbQ{}].    (|(a  *  r)  -  a  *  s|  =  (|r  -  s|  *  |a|))


By

---

Latex:
xxx(Auto  THEN  (Subst'  ((a  *  r)  -  a  *  s)  =  ((r  -  s)  *  a)  0  THENA  Auto))xxx

---

Home Index