---

Step * 1 1 of Lemma q-elim


1. r : ℚ
2. qrep(r) = r ∈ ℚ
3. v1 : ℤ
4. v2 : ℕ+
⊢ ∃p:ℤ. ∃q:ℕ+. ((¬(q = 0 ∈ ℚ)) c∧ (<v1, v2> = (p/q) ∈ ℚ))
BY
{ (Assert <v1, v2> ~ (v1/v2) BY
         (RepUR ``qdiv qmul qinv`` 0
          THEN ((CallByValueReduceOn ⌜v1⌝ 0⋅ THENA Auto)
                THEN (CallByValueReduceOn ⌜v2⌝ 0⋅ THENA Auto)
                THEN (Reduce 0 THENA Auto)
                THEN (CallByValueReduce 0 THENA Auto)
                THEN (Reduce 0 THENA Auto))
          THEN EqCD
          THEN Auto))⋅ }

1
1. r : ℚ
2. qrep(r) = r ∈ ℚ
3. v1 : ℤ
4. v2 : ℕ+
5. <v1, v2> ~ (v1/v2)
⊢ ∃p:ℤ. ∃q:ℕ+. ((¬(q = 0 ∈ ℚ)) c∧ (<v1, v2> = (p/q) ∈ ℚ))

---

Latex:

---

Latex:

1.  r  :  \mBbbQ{}
2.  qrep(r)  =  r
3.  v1  :  \mBbbZ{}
4.  v2  :  \mBbbN{}\msupplus{}
\mvdash{}  \mexists{}p:\mBbbZ{}.  \mexists{}q:\mBbbN{}\msupplus{}.  ((\mneg{}(q  =  0))  c\mwedge{}  (<v1,  v2>  =  (p/q)))


By

---

Latex:
(Assert  <v1,  v2>  \msim{}  (v1/v2)  BY
              (RepUR  ``qdiv  qmul  qinv``  0
                THEN  ((CallByValueReduceOn  \mkleeneopen{}v1\mkleeneclose{}  0\mcdot{}  THENA  Auto)
                            THEN  (CallByValueReduceOn  \mkleeneopen{}v2\mkleeneclose{}  0\mcdot{}  THENA  Auto)
                            THEN  (Reduce  0  THENA  Auto)
                            THEN  (CallByValueReduce  0  THENA  Auto)
                            THEN  (Reduce  0  THENA  Auto))
                THEN  EqCD
                THEN  Auto))\mcdot{}

---

Home Index