---

Step * 1 of Lemma coprime_iff_ndivides


1. a : ℤ
2. p : ℤ
3. prime(p)
4. CoPrime(p,a)
⊢ ¬(p | a)
BY
{ ((RWO "coprime_elim" 4 THENM D 0) THENA Auto) }

1
1. a : ℤ
2. p : ℤ
3. prime(p)
4. ∀c:ℤ. ((c | p) ⇒ (c | a) ⇒ (c ~ 1))
5. p | a
⊢ False

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  p  :  \mBbbZ{}
3.  prime(p)
4.  CoPrime(p,a)
\mvdash{}  \mneg{}(p  |  a)


By

---

Latex:
((RWO  "coprime\_elim"  4  THENM  D  0)  THENA  Auto)

---

Home Index