---

Step * 2 1 of Lemma qrep-coprime

.....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. ¬(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
BY
{ Assert ⌜CoPrime(-v3,-v4)⌝⋅ }

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. ¬(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) ∈ ℤ
⊢ CoPrime(-v3,-v4)

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

---

Latex:

---

Latex:
.....assertion..... 
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)
\mvdash{}  gcd(-v3;-v4)  \msim{}  1


By

---

Latex:
Assert  \mkleeneopen{}CoPrime(-v3,-v4)\mkleeneclose{}\mcdot{}

---

Home Index