---

Step * 2 of Lemma qabs-zero


1. r : ℚ
2. |r| = 0 ∈ ℚ
⊢ r = 0 ∈ ℚ
BY
{ xxx(Unfold `qabs` -1 THEN (CallByValueReduce (-1) THENA Auto))xxx }

1
1. r : ℚ
2. if qpositive(r) then r else -(r) fi  = 0 ∈ ℚ
⊢ r = 0 ∈ ℚ

---

Latex:

---

Latex:

1.  r  :  \mBbbQ{}
2.  |r|  =  0
\mvdash{}  r  =  0


By

---

Latex:
xxx(Unfold  `qabs`  -1  THEN  (CallByValueReduce  (-1)  THENA  Auto))xxx

---

Home Index