---

Step * 1 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. 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 ∈ ℤ
BY
{ Assert ⌜gcd(v3;v4) ~ 1⌝⋅ }

1
.....assertion..... 
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. 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) ∈ ℤ
17. gcd(v3;v4) ~ 1
⊢ |gcd(v3;v4)| = 1 ∈ ℤ

---

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.  gcd\_reduce(p  *  1;q)  =  <v1,  v3,  v4>
12.  0  \mleq{}  v4
13.  (p  *  1)  =  (v3  *  v1)
14.  q  =  (v4  *  v1)
15.  CoPrime(v3,v4)
16.  ((p  *  1)  *  v4)  =  (v3  *  q)
\mvdash{}  |gcd(v3;v4)|  =  1


By

---

Latex:
Assert  \mkleeneopen{}gcd(v3;v4)  \msim{}  1\mkleeneclose{}\mcdot{}

---

Home Index