---

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

.....assertion..... 
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
⊢ <(-1) * q, p> = <q, (-1) * p> ∈ ℚ
BY
{ ((Fold `mk-rational` 0 THEN (RWO "mk-rational-qdiv" 0 THENA Auto)) THEN CaseNat 0 `p') }

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

2
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) ∈ ℚ

---

Latex:

---

Latex:
.....assertion..... 
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
\mvdash{}  <(-1)  *  q,  p>  =  <q,  (-1)  *  p>


By

---

Latex:
((Fold  `mk-rational`  0  THEN  (RWO  "mk-rational-qdiv"  0  THENA  Auto))  THEN  CaseNat  0  `p')

---

Home Index