---

Step * 2 1 of Lemma qabs-zero


1. r : ℚ
2. if qpositive(r) then r else -(r) fi  = 0 ∈ ℚ
⊢ r = 0 ∈ ℚ
BY
{ (SplitOnHypITE -1 ⋅ THEN Auto) }

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

---

Latex:

---

Latex:

1.  r  :  \mBbbQ{}
2.  if  qpositive(r)  then  r  else  -(r)  fi    =  0
\mvdash{}  r  =  0


By

---

Latex:
(SplitOnHypITE  -1  \mcdot{}  THEN  Auto)

---

Home Index