---

Step * 2 1 1 1 of Lemma qabs-qinv


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)| ∈ ℚ
BY
{ (Unfold `qabs` 0 THEN (CallByValueReduce 0 THENA 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 ∈ ℚ)
⊢ if qpositive(1/(p/q)) then 1/(p/q) else -(1/(p/q)) fi  = 1/if qpositive((p/q)) then (p/q) else -((p/q)) fi  ∈ ℚ

---

Latex:

---

Latex:

1.  s  :  \mBbbQ{}
2.  \mneg{}(s  =  0)
3.  p  :  \mBbbZ{}
4.  q  :  \mBbbZ{}
5.  0  <  q
6.  \mneg{}(q  =  0)
7.  s  =  (p/q)
8.  \mneg{}\muparrow{}qeq(q;0)
9.  \mneg{}((p/q)  =  0)
10.  \mneg{}(|(p/q)|  =  0)
\mvdash{}  |1/(p/q)|  =  1/|(p/q)|


By

---

Latex:
(Unfold  `qabs`  0  THEN  (CallByValueReduce  0  THENA  Auto))

---

Home Index