---

Step * 2 1 1 1 1 1 2 1 2 of Lemma qabs-qinv


1. s : ℚ
2. ¬(s = 0 ∈ ℚ)
3. p : ℤ
4. ¬0 < p
5. q : ℤ
6. 0 < q
7. ¬(q = 0 ∈ ℚ)
8. s = (p/q) ∈ ℚ
9. ¬↑qeq(q;0)
10. ¬((p/q) = 0 ∈ ℚ)
11. ¬(|(p/q)| = 0 ∈ ℚ)
12. 0 < q
13. ¬(p = 0 ∈ ℤ)
⊢ ((-1) * q/p) = (q/(-1) * p) ∈ ℚ
BY
{ (QMul ⌜(-1) * p⌝ 0⋅ THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(QMul  \mkleeneopen{}(-1)  *  p\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index