---

Step * of Lemma coprime_elim

∀a,b:ℤ.  (CoPrime(a,b) ⇐⇒ ∀c:ℤ. ((c | a) ⇒ (c | b) ⇒ (c ~ 1)))
BY
{ (((RepUnfolds ``coprime gcd_p assoced`` 0 THENM GenRepD) THENM Try (BLemma `one_divs_any`)) THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(((RepUnfolds  ``coprime  gcd\_p  assoced``  0  THENM  GenRepD)  THENM  Try  (BLemma  `one\_divs\_any`))
  THEN  Auto
  )

---

Home Index