---

Step * 2 1 1 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 ∈ ℚ)
⊢ if (0 <z q ∧b 0 <z p) ∨b(q <z 0 ∧b p <z 0) then <q, p> else <(-1) * q, p> fi 
= let r' ⟵ if (0 <z p ∧b 0 <z q) ∨b(p <z 0 ∧b q <z 0) 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
{ RepeatFor 2 (AutoSplit) }

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

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
⊢ <(-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.  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{}  if  (0  <z  q  \mwedge{}\msubb{}  0  <z  p)  \mvee{}\msubb{}(q  <z  0  \mwedge{}\msubb{}  p  <z  0)  then  <q,  p>  else  <(-1)  *  q,  p>  fi 
=  let  r'  \mleftarrow{}{}  if  (0  <z  p  \mwedge{}\msubb{}  0  <z  q)  \mvee{}\msubb{}(p  <z  0  \mwedge{}\msubb{}  q  <z  0)  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:
RepeatFor  2  (AutoSplit)

---

Home Index