---

Step * 2 1 of Lemma qabs-qinv


1. s : ℚ
2. ¬(s = 0 ∈ ℚ)
3. ¬(s = 0 ∈ ℚ)
4. ¬(|s| = 0 ∈ ℚ)
⊢ |1/s| = 1/|s| ∈ ℚ
BY
{ RepeatFor 2 (MoveToConcl (-1)) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
RepeatFor  2  (MoveToConcl  (-1))

---

Home Index