---

Step * of Lemma gcd_of_triple

∀a,b,c,x,y:ℤ.
  (GCD(a;b;x) ⇒ GCD(x;c;y) ⇒ (((y | a) ∧ (y | b) ∧ (y | c)) ∧ (∀z:ℤ. ((z | a) ⇒ (z | b) ⇒ (z | c) ⇒ (z | y)))))
BY
{ (Unfold `gcd_p` 0 THEN Auto THEN RelRST THEN Auto) }

---

Latex:

---

Latex:
\mforall{}a,b,c,x,y:\mBbbZ{}.
    (GCD(a;b;x)
    {}\mRightarrow{}  GCD(x;c;y)
    {}\mRightarrow{}  (((y  |  a)  \mwedge{}  (y  |  b)  \mwedge{}  (y  |  c))  \mwedge{}  (\mforall{}z:\mBbbZ{}.  ((z  |  a)  {}\mRightarrow{}  (z  |  b)  {}\mRightarrow{}  (z  |  c)  {}\mRightarrow{}  (z  |  y)))))


By

---

Latex:
(Unfold  `gcd\_p`  0  THEN  Auto  THEN  RelRST  THEN  Auto)

---

Home Index