---

Step * 2 of Lemma coprime_iff_ndivides


1. a : ℤ
2. p : ℤ
3. prime(p)
4. ¬(p | a)
⊢ CoPrime(p,a)
BY
{ ((BLemma `coprime_intro` THENM RepD) THENA Auto) }

1
1. a : ℤ
2. p : ℤ
3. prime(p)
4. ¬(p | a)
5. c : ℤ
6. c | p
7. c | a
⊢ c | 1

---

Latex:

---

Latex:

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


By

---

Latex:
((BLemma  `coprime\_intro`  THENM  RepD)  THENA  Auto)

---

Home Index