---

Step * of Lemma better-gcd-properties

∀a,b:ℤ.
  ((∃c:ℤ. ((c * better-gcd(a;b)) = a ∈ ℤ))
  ∧ (∃d:ℤ. ((d * better-gcd(a;b)) = b ∈ ℤ))
  ∧ (∃s,t:ℤ. (better-gcd(a;b) = ((s * a) + (t * b)) ∈ ℤ)))
BY
{ (InstLemma `gcd-properties` [] THEN RepeatFor 2 (ParallelLast') THEN RWO "better-gcd-gcd" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbZ{}.
    ((\mexists{}c:\mBbbZ{}.  ((c  *  better-gcd(a;b))  =  a))
    \mwedge{}  (\mexists{}d:\mBbbZ{}.  ((d  *  better-gcd(a;b))  =  b))
    \mwedge{}  (\mexists{}s,t:\mBbbZ{}.  (better-gcd(a;b)  =  ((s  *  a)  +  (t  *  b)))))


By

---

Latex:
(InstLemma  `gcd-properties`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  RWO  "better-gcd-gcd"  0
  THEN  Auto)

---

Home Index