---

Step * of Lemma gcd-property

∀x,y:ℤ.  ∃a,b:ℤ. (CoPrime(a,b) ∧ (x = (gcd(x;y) * a) ∈ ℤ) ∧ (y = (gcd(x;y) * b) ∈ ℤ))
BY
{ (Auto
   THEN ((InstLemma `gcd_is_divisor_1` [⌜x⌝; ⌜y⌝])⋅ THENA Auto)
   THEN D -1
   THEN ((InstLemma `gcd_is_divisor_2` [⌜x⌝; ⌜y⌝])⋅ THENA Auto)
   THEN D -1
   THEN (Decide gcd(x;y) = 0 ∈ ℤ THENA Auto)) }

1
1. x : ℤ
2. y : ℤ
3. c : ℤ
4. x = (gcd(x;y) * c) ∈ ℤ
5. c1 : ℤ
6. y = (gcd(x;y) * c1) ∈ ℤ
7. gcd(x;y) = 0 ∈ ℤ
⊢ ∃a,b:ℤ. (CoPrime(a,b) ∧ (x = (gcd(x;y) * a) ∈ ℤ) ∧ (y = (gcd(x;y) * b) ∈ ℤ))

2
1. x : ℤ
2. y : ℤ
3. c : ℤ
4. x = (gcd(x;y) * c) ∈ ℤ
5. c1 : ℤ
6. y = (gcd(x;y) * c1) ∈ ℤ
7. ¬(gcd(x;y) = 0 ∈ ℤ)
⊢ ∃a,b:ℤ. (CoPrime(a,b) ∧ (x = (gcd(x;y) * a) ∈ ℤ) ∧ (y = (gcd(x;y) * b) ∈ ℤ))

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbZ{}.    \mexists{}a,b:\mBbbZ{}.  (CoPrime(a,b)  \mwedge{}  (x  =  (gcd(x;y)  *  a))  \mwedge{}  (y  =  (gcd(x;y)  *  b)))


By

---

Latex:
(Auto
  THEN  ((InstLemma  `gcd\_is\_divisor\_1`  [\mkleeneopen{}x\mkleeneclose{};  \mkleeneopen{}y\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  ((InstLemma  `gcd\_is\_divisor\_2`  [\mkleeneopen{}x\mkleeneclose{};  \mkleeneopen{}y\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  (Decide  gcd(x;y)  =  0  THENA  Auto))

---

Home Index