---

Step * 2 2 of Lemma qrep-coprime


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) ∈ ℤ
17. gcd(-v3;-v4) ~ 1
⊢ |gcd(-v3;-v4)| = 1 ∈ ℤ
BY
{ ((FLemma `assoced_elim` [-1] THEN Auto) THEN D -1 THEN HypSubst' (-1) 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  r  :  \mBbbQ{}
2.  p  :  \mBbbZ{}
3.  q  :  \mBbbZ{}
4.  0  <  q
5.  \mneg{}(q  =  0)
6.  r  =  (p/q)
7.  \mneg{}\muparrow{}qeq(q;0)
8.  v1  :  \mBbbN{}@i
9.  v3  :  \mBbbZ{}@i
10.  v4  :  \mBbbZ{}@i
11.  \mneg{}(0  \mleq{}  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)
17.  gcd(-v3;-v4)  \msim{}  1
\mvdash{}  |gcd(-v3;-v4)|  =  1


By

---

Latex:
((FLemma  `assoced\_elim`  [-1]  THEN  Auto)  THEN  D  -1  THEN  HypSubst'  (-1)  0  THEN  Auto)\mcdot{}

---

Home Index