---

Step * 2 of Lemma qabs-qinv


1. s : {s:ℚ| ¬(s = 0 ∈ ℚ)} 
2. (¬(s = 0 ∈ ℚ)) ∧ (¬(|s| = 0 ∈ ℚ))
⊢ |1/s| = 1/|s| ∈ ℚ
BY
{ (D 1 THEN Auto) }

1
1. s : ℚ
2. ¬(s = 0 ∈ ℚ)
3. ¬(s = 0 ∈ ℚ)
4. ¬(|s| = 0 ∈ ℚ)
⊢ |1/s| = 1/|s| ∈ ℚ

---

Latex:

---

Latex:

1.  s  :  \{s:\mBbbQ{}|  \mneg{}(s  =  0)\} 
2.  (\mneg{}(s  =  0))  \mwedge{}  (\mneg{}(|s|  =  0))
\mvdash{}  |1/s|  =  1/|s|


By

---

Latex:
(D  1  THEN  Auto)

---

Home Index