---

Step * 2 1 1 1 1 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
⊢ <(-1) * q, p>
= let r' ⟵ if p <z 0 ∧b ff then <p, q> else <(-1) * p, q> fi 
  in if isint(r') then <1, r'> else let p,q = r' in <q, p> fi 
∈ ℚ
BY
{ Assert ⌜<(-1) * q, p> = <q, (-1) * p> ∈ ℚ⌝⋅ }

1
.....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> ∈ ℚ

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. <(-1) * q, p> = <q, (-1) * p> ∈ ℚ
⊢ <(-1) * q, p>
= let r' ⟵ if p <z 0 ∧b ff then <p, q> else <(-1) * p, q> fi 
  in if isint(r') then <1, r'> else let p,q = r' in <q, p> fi 
∈ ℚ

---

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
\mvdash{}  <(-1)  *  q,  p>
=  let  r'  \mleftarrow{}{}  if  p  <z  0  \mwedge{}\msubb{}  ff  then  <p,  q>  else  <(-1)  *  p,  q>  fi 
    in  if  isint(r')  then  ə,  r'>  else  let  p,q  =  r'  in  <q,  p>  fi 


By

---

Latex:
Assert  \mkleeneopen{}<(-1)  *  q,  p>  =  <q,  (-1)  *  p>\mkleeneclose{}\mcdot{}

---

Home Index