---

Step * of Lemma qabs-qminus

∀[r:ℚ]. (|r| = |-(r)| ∈ ℚ)
BY
{ xxx(RWO "qabs-qmul" 0 THEN Auto)xxx }

1
1. r : ℚ
⊢ |r| = (|-1| * |r|) ∈ ℚ

---

Latex:

---

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


By

---

Latex:
xxx(RWO  "qabs-qmul"  0  THEN  Auto)xxx

---

Home Index