---

Step * 1 1 of Lemma qabs-qinv


1. s : ℚ
2. ¬(s = 0 ∈ ℚ)
3. ¬(s = 0 ∈ ℚ)
4. |s| = 0 ∈ ℚ
⊢ False
BY
{ (RWO "qabs-zero<" (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  \mBbbQ{}
2.  \mneg{}(s  =  0)
3.  \mneg{}(s  =  0)
4.  |s|  =  0
\mvdash{}  False


By

---

Latex:
(RWO  "qabs-zero<"  (-1)  THEN  Auto)

---

Home Index