---

Step * of Lemma coprime_intro

∀a,b:ℤ.  ((∀c:ℤ. ((c | a) ⇒ (c | b) ⇒ (c | 1))) ⇒ CoPrime(a,b))
BY
{ ((RepUnfolds ``coprime gcd_p`` 0 THENM Backchain ``new_hyps one_divs_any``) THENA Auto) }

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbZ{}.    ((\mforall{}c:\mBbbZ{}.  ((c  |  a)  {}\mRightarrow{}  (c  |  b)  {}\mRightarrow{}  (c  |  1)))  {}\mRightarrow{}  CoPrime(a,b))


By

---

Latex:
((RepUnfolds  ``coprime  gcd\_p``  0  THENM  Backchain  ``new\_hyps  one\_divs\_any``)  THENA  Auto)

---

Home Index