---

Step * 2 1 1 1 1 1 2 1 1 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/0) = (q/(-1) * 0) ∈ ℚ
BY
{ (D (-4) THEN HypSubst' (-1) 0) }

1
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. 0 < q
12. p = 0 ∈ ℤ
⊢ (0/q) = 0 ∈ ℚ

---

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.  p  =  0
\mvdash{}  ((-1)  *  q/0)  =  (q/(-1)  *  0)


By

---

Latex:
(D  (-4)  THEN  HypSubst'  (-1)  0)

---

Home Index