---

Step * of Lemma qabs-qmul-case1

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

1
1. r : ℚ
2. s : ℚ
3. a : ℚ
⊢ |(r - s) * a| = (|r - s| * |a|) ∈ ℚ

---

Latex:

---

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


By

---

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

---

Home Index