---

Step * 2 1 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) ∈ ℤ
⊢ CoPrime(-v3,-v4)
BY
{ ((FLemma `coprime_bezout_id1` [-2] THENM ExRepD)
   THEN Auto
   THEN (BLemma `coprime_bezout_id2` THENA Auto)
   THEN InstConcl [⌜-x⌝;⌜-y⌝]⋅
   THEN Auto) }

---

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{}  CoPrime(-v3,-v4)


By

---

Latex:
((FLemma  `coprime\_bezout\_id1`  [-2]  THENM  ExRepD)
  THEN  Auto
  THEN  (BLemma  `coprime\_bezout\_id2`  THENA  Auto)
  THEN  InstConcl  [\mkleeneopen{}-x\mkleeneclose{};\mkleeneopen{}-y\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index