---

Step * of Lemma qrep-coprime

No Annotations
∀[r:ℚ]. (|gcd(fst(qrep(r));snd(qrep(r)))| = 1 ∈ ℤ)
BY
{ (((Auto THEN ElimRationals) THENA Auto)
   THEN RepUR ``qrep qdiv qmul qinv`` 0
   THEN (CallByValueReduce 0 THENA Auto)
   THEN (Reduce 0 THEN Auto THEN (RW (SweepUpC CallByValueallC) 0 THEN ((Reduce 0 THENA Auto) THEN Auto)⋅)⋅)
   THEN (InstLemma `gcd_reduce_property` [⌜p * 1⌝;⌜q⌝]⋅ THEN Auto)
   THEN MoveToConcl (-1)
   THEN GenConclAtAddr [1;1]
   THEN RepeatFor 2 (D -2)
   THEN Reduce 0
   THEN AutoSplit
   THEN Auto) }

1
1. r : ℚ
2. p : ℤ
3. q : ℤ
4. 0 < q
5. ¬(q = 0 ∈ ℚ)
6. r = (p/q) ∈ ℚ
7. ¬↑qeq(q;0)
8. v1 : ℕ@i
9. v3 : ℤ@i
10. v4 : ℤ@i
11. gcd_reduce(p * 1;q) = <v1, v3, v4> ∈ (ℕ × ℤ × ℤ)
12. 0 ≤ v4
13. (p * 1) = (v3 * v1) ∈ ℤ
14. q = (v4 * v1) ∈ ℤ
15. CoPrime(v3,v4)
16. ((p * 1) * v4) = (v3 * q) ∈ ℤ
⊢ |gcd(v3;v4)| = 1 ∈ ℤ

2
1. r : ℚ
2. p : ℤ
3. q : ℤ
4. 0 < q
5. ¬(q = 0 ∈ ℚ)
6. r = (p/q) ∈ ℚ
7. ¬↑qeq(q;0)
8. v1 : ℕ@i
9. v3 : ℤ@i
10. v4 : ℤ@i
11. ¬(0 ≤ v4)
12. gcd_reduce(p * 1;q) = <v1, v3, v4> ∈ (ℕ × ℤ × ℤ)
13. (p * 1) = (v3 * v1) ∈ ℤ
14. q = (v4 * v1) ∈ ℤ
15. CoPrime(v3,v4)
16. ((p * 1) * v4) = (v3 * q) ∈ ℤ
⊢ |gcd(-v3;-v4)| = 1 ∈ ℤ

---

Latex:

---

Latex:
No  Annotations
\mforall{}[r:\mBbbQ{}].  (|gcd(fst(qrep(r));snd(qrep(r)))|  =  1)


By

---

Latex:
(((Auto  THEN  ElimRationals)  THENA  Auto)
  THEN  RepUR  ``qrep  qdiv  qmul  qinv``  0
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  (Reduce  0
              THEN  Auto
              THEN  (RW  (SweepUpC  CallByValueallC)  0  THEN  ((Reduce  0  THENA  Auto)  THEN  Auto)\mcdot{})\mcdot{})
  THEN  (InstLemma  `gcd\_reduce\_property`  [\mkleeneopen{}p  *  1\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  MoveToConcl  (-1)
  THEN  GenConclAtAddr  [1;1]
  THEN  RepeatFor  2  (D  -2)
  THEN  Reduce  0
  THEN  AutoSplit
  THEN  Auto)

---

Home Index