---

Step * 2 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 qpositive(1/(p/q)) then 1/(p/q) else -(1/(p/q)) fi  = 1/if qpositive((p/q)) then (p/q) else -((p/q)) fi  ∈ ℚ
BY
{ (RepUR ``qdiv qinv qabs qmul qpositive`` 0⋅
   THEN (CallByValueReduceOn ⌜q⌝ 0⋅ THENA Auto)
   THEN (CallByValueReduceOn ⌜p⌝ 0⋅ THENA Auto)
   THEN Reduce 0
   THEN Auto
   THEN (CallByValueReduceOn ⌜<1, q>⌝ 0⋅ THENA Auto)
   THEN Reduce 0
   THEN Subst' p * 1 ~ p 0
   THEN Auto
   THEN (CallByValueReduceOn ⌜<p, q>⌝ 0⋅ THENA Auto)
   THEN Reduce 0
   THEN (CallByValueReduceOn ⌜<q, p>⌝ 0⋅ THENA Auto)
   THEN Reduce 0) }

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

---

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  qpositive(1/(p/q))  then  1/(p/q)  else  -(1/(p/q))  fi 
=  1/if  qpositive((p/q))  then  (p/q)  else  -((p/q))  fi 


By

---

Latex:
(RepUR  ``qdiv  qinv  qabs  qmul  qpositive``  0\mcdot{}
  THEN  (CallByValueReduceOn  \mkleeneopen{}q\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduceOn  \mkleeneopen{}p\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  Reduce  0
  THEN  Auto
  THEN  (CallByValueReduceOn  \mkleeneopen{}ə,  q>\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  Reduce  0
  THEN  Subst'  p  *  1  \msim{}  p  0
  THEN  Auto
  THEN  (CallByValueReduceOn  \mkleeneopen{}<p,  q>\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  Reduce  0
  THEN  (CallByValueReduceOn  \mkleeneopen{}<q,  p>\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  Reduce  0)

---

Home Index