---

Step * 2 1 1 1 of Lemma qabs-zero


1. r : ℚ
2. -(r) = 0 ∈ ℚ
3. ¬↑qpositive(r)
⊢ -(-(r)) = 0 ∈ ℚ
BY
{ xxx(xxxHypSubst' -2 0xxx THEN Auto)xxx }

---

Latex:

---

Latex:

1.  r  :  \mBbbQ{}
2.  -(r)  =  0
3.  \mneg{}\muparrow{}qpositive(r)
\mvdash{}  -(-(r))  =  0


By

---

Latex:
xxx(xxxHypSubst'  -2  0xxx  THEN  Auto)xxx

---

Home Index