---

Step * 2 1 of Lemma assert-is-qrep


1. p : ℤ × ℕ+
2. q : ℚ
3. qrep(q) = p ∈ (ℤ × ℕ+)
⊢ ↑is-qrep(qrep(q))
BY
{ xxx((InstLemma `qrep-coprime` [⌜q⌝]⋅ THENA Auto)
      THEN MoveToConcl (-1)
      THEN GenConclAtAddr [2;1;1]
      THEN D -2
      THEN RepUR ``is-qrep`` 0
      THEN All Thin)xxx }

1
1. v1 : ℤ
2. v2 : ℕ+
⊢ (|gcd(v1;v2)| = 1 ∈ ℤ) ⇒ (↑eval g = better-gcd(v1;v2) in (g =z 1) ∨b(g =z -1))

---

Latex:

---

Latex:

1.  p  :  \mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}
2.  q  :  \mBbbQ{}
3.  qrep(q)  =  p
\mvdash{}  \muparrow{}is-qrep(qrep(q))


By

---

Latex:
xxx((InstLemma  `qrep-coprime`  [\mkleeneopen{}q\mkleeneclose{}]\mcdot{}  THENA  Auto)
        THEN  MoveToConcl  (-1)
        THEN  GenConclAtAddr  [2;1;1]
        THEN  D  -2
        THEN  RepUR  ``is-qrep``  0
        THEN  All  Thin)xxx

---

Home Index