---

Step * 2 of Lemma gcd-property


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) ∈ ℤ))
BY
{ ((InstConcl [⌜c⌝; ⌜c1⌝])⋅
   THEN Auto
   THEN BLemma `coprime_bezout_id`
   THEN Auto
   THEN (Assert ∃u,v:ℤ. (gcd(x;y) = ((u * x) + (v * y)) ∈ ℤ) BY
               (((InstLemma `bezout_ident` [⌜x⌝; ⌜y⌝])⋅ THENA Auto)
                THEN ExRepD
                THEN ((InstLemma `gcd_sat_pred` [⌜x⌝; ⌜y⌝])⋅ THENA Auto)
                THEN ((FLemma `gcd_unique` [-1; -2]) THENA Auto)
                THEN ((RWO "assoced_elim" (-1)) THENA Auto)
                THEN D -1
                THEN Auto
                THEN (InstConcl [⌜-u⌝; ⌜-v⌝])⋅
                THEN 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 ∈ ℤ)
8. ∃u,v:ℤ. (gcd(x;y) = ((u * x) + (v * y)) ∈ ℤ)
⊢ ∃x,y:ℤ. (((c * x) + (c1 * y)) = 1 ∈ ℤ)

---

Latex:

---

Latex:

1.  x  :  \mBbbZ{}
2.  y  :  \mBbbZ{}
3.  c  :  \mBbbZ{}
4.  x  =  (gcd(x;y)  *  c)
5.  c1  :  \mBbbZ{}
6.  y  =  (gcd(x;y)  *  c1)
7.  \mneg{}(gcd(x;y)  =  0)
\mvdash{}  \mexists{}a,b:\mBbbZ{}.  (CoPrime(a,b)  \mwedge{}  (x  =  (gcd(x;y)  *  a))  \mwedge{}  (y  =  (gcd(x;y)  *  b)))


By

---

Latex:
((InstConcl  [\mkleeneopen{}c\mkleeneclose{};  \mkleeneopen{}c1\mkleeneclose{}])\mcdot{}
  THEN  Auto
  THEN  BLemma  `coprime\_bezout\_id`
  THEN  Auto
  THEN  (Assert  \mexists{}u,v:\mBbbZ{}.  (gcd(x;y)  =  ((u  *  x)  +  (v  *  y)))  BY
                          (((InstLemma  `bezout\_ident`  [\mkleeneopen{}x\mkleeneclose{};  \mkleeneopen{}y\mkleeneclose{}])\mcdot{}  THENA  Auto)
                            THEN  ExRepD
                            THEN  ((InstLemma  `gcd\_sat\_pred`  [\mkleeneopen{}x\mkleeneclose{};  \mkleeneopen{}y\mkleeneclose{}])\mcdot{}  THENA  Auto)
                            THEN  ((FLemma  `gcd\_unique`  [-1;  -2])  THENA  Auto)
                            THEN  ((RWO  "assoced\_elim"  (-1))  THENA  Auto)
                            THEN  D  -1
                            THEN  Auto
                            THEN  (InstConcl  [\mkleeneopen{}-u\mkleeneclose{};  \mkleeneopen{}-v\mkleeneclose{}])\mcdot{}
                            THEN  Auto)))

---

Home Index