---

Step * 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. 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
{ ((D 0 THEN Auto)
   THEN RepeatFor 2 (D (-2))
   THEN BHyp -2
   THEN Auto
   THEN Try ((BLemma `gcd_is_divisor_1`  THEN Auto))
   THEN Try ((BLemma `gcd_is_divisor_2`  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.  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)  \msim{}  1


By

---

Latex:
((D  0  THEN  Auto)
  THEN  RepeatFor  2  (D  (-2))
  THEN  BHyp  -2
  THEN  Auto
  THEN  Try  ((BLemma  `gcd\_is\_divisor\_1`    THEN  Auto))
  THEN  Try  ((BLemma  `gcd\_is\_divisor\_2`    THEN  Auto)))

---

Home Index