---

Step * 2 1 1 of Lemma qabs-qinv


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

1
1. s : ℚ
2. ¬(s = 0 ∈ ℚ)
3. p : ℤ
4. q : ℤ
5. 0 < q
6. ¬(q = 0 ∈ ℚ)
7. s = (p/q) ∈ ℚ
8. ¬↑qeq(q;0)
9. ¬((p/q) = 0 ∈ ℚ)
10. ¬(|(p/q)| = 0 ∈ ℚ)
⊢ |1/(p/q)| = 1/|(p/q)| ∈ ℚ

---

Latex:

---

Latex:

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


By

---

Latex:
(ElimRationals\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index