---

Step * 2 1 1 of Lemma qabs-zero

.....falsecase..... 
1. r : ℚ
2. -(r) = 0 ∈ ℚ
3. ¬↑qpositive(r)
⊢ r = 0 ∈ ℚ
BY
{ xxx(Subst ⌜r = -(-(r)) ∈ ℚ⌝ 0⋅ THENA Auto)xxx }

1
1. r : ℚ
2. -(r) = 0 ∈ ℚ
3. ¬↑qpositive(r)
⊢ -(-(r)) = 0 ∈ ℚ

---

Latex:

---

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


By

---

Latex:
xxx(Subst  \mkleeneopen{}r  =  -(-(r))\mkleeneclose{}  0\mcdot{}  THENA  Auto)xxx

---

Home Index