---

Step * of Lemma gcd_reduce_property

∀p,q:ℤ.  let g,a,b = gcd_reduce(p;q) in (p = (a * g) ∈ ℤ) ∧ (q = (b * g) ∈ ℤ) ∧ CoPrime(a,b) ∧ ((p * b) = (a * q) ∈ ℤ)
BY
{ (TACTIC:Auto
   THEN Unfold `gcd_reduce` 0
   THEN TACTIC:((GenConclAtAddr [1;1] THENA Auto)
                THEN (Thin (-1))
                THEN RepeatFor 3 (TACTIC:D -1)
                THEN ExRepD
                THEN RepUR ``spreadn`` 0
                THEN Auto)) }

1
1. p : ℤ
2. q : ℤ
3. g : ℕ
4. a : ℤ
5. b : ℤ
6. x : ℤ
7. y : ℤ
8. v6 : p = (a * g) ∈ ℤ
9. v8 : q = (b * g) ∈ ℤ
10. v9 : ((x * a) + (y * b)) = 1 ∈ ℤ
11. p = (a * g) ∈ ℤ
12. q = (b * g) ∈ ℤ
⊢ CoPrime(a,b)

2
1. p : ℤ
2. q : ℤ
3. g : ℕ
4. a : ℤ
5. b : ℤ
6. x : ℤ
7. y : ℤ
8. v6 : p = (a * g) ∈ ℤ
9. v8 : q = (b * g) ∈ ℤ
10. v9 : ((x * a) + (y * b)) = 1 ∈ ℤ
11. p = (a * g) ∈ ℤ
12. q = (b * g) ∈ ℤ
13. CoPrime(a,b)
⊢ (p * b) = (a * q) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}p,q:\mBbbZ{}.
    let  g,a,b  =  gcd\_reduce(p;q)  in 
    (p  =  (a  *  g))  \mwedge{}  (q  =  (b  *  g))  \mwedge{}  CoPrime(a,b)  \mwedge{}  ((p  *  b)  =  (a  *  q))


By

---

Latex:
(TACTIC:Auto
  THEN  Unfold  `gcd\_reduce`  0
  THEN  TACTIC:((GenConclAtAddr  [1;1]  THENA  Auto)
                            THEN  (Thin  (-1))
                            THEN  RepeatFor  3  (TACTIC:D  -1)
                            THEN  ExRepD
                            THEN  RepUR  ``spreadn``  0
                            THEN  Auto))

---

Home Index