---

Step * 2 1 of Lemma coprime_iff_ndivides


1. a : ℤ
2. p : ℤ
3. prime(p)
4. ¬(p | a)
5. c : ℤ
6. c | p
7. c | a
⊢ c | 1
BY
{ (((Sel (-1) (FLemma `prime_elim` [3]) THENM RepD) THENA Auto)
   THEN (FHyp 10 [6] THENA Auto)
   THEN Unfold `assoced` 11
   THEN (GenExRepD THEN Try (Complete (Auto)))
   THEN RelRST
   THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  p  :  \mBbbZ{}
3.  prime(p)
4.  \mneg{}(p  |  a)
5.  c  :  \mBbbZ{}
6.  c  |  p
7.  c  |  a
\mvdash{}  c  |  1


By

---

Latex:
(((Sel  (-1)  (FLemma  `prime\_elim`  [3])  THENM  RepD)  THENA  Auto)
  THEN  (FHyp  10  [6]  THENA  Auto)
  THEN  Unfold  `assoced`  11
  THEN  (GenExRepD  THEN  Try  (Complete  (Auto)))
  THEN  RelRST
  THEN  Auto)

---

Home Index