---

Step * 1 of Lemma gcd-prime


1. p : ℕ
2. prime(p)
3. n : {1..p-}
4. ¬(p = 0 ∈ ℤ)
5. ¬(p ~ 1)
6. ∀a:ℤ. ((a | p) ⇒ ((a ~ 1) ∨ (a ~ p)))
7. gcd(n;p) | n
8. gcd(n;p) | p
9. ∀z:ℤ. (((z | n) ∧ (z | p)) ⇒ (z | gcd(n;p)))
⊢ gcd(n;p) = 1 ∈ ℤ
BY
{ ((FHyp 6 [-2] THEN Auto)
   THEN RWO "assoced_elim" (-1)
   THEN Auto
   THEN InstLemma `gcd-positive` [⌜p⌝;⌜n⌝]⋅
   THEN Auto
   THEN SplitOrHyps
   THEN Auto') }

1
1. p : ℕ
2. prime(p)
3. n : {1..p-}
4. ¬(p = 0 ∈ ℤ)
5. ¬(p ~ 1)
6. ∀a:ℤ. ((a | p) ⇒ ((a ~ 1) ∨ (a ~ p)))
7. gcd(n;p) | n
8. gcd(n;p) | p
9. ∀z:ℤ. (((z | n) ∧ (z | p)) ⇒ (z | gcd(n;p)))
10. gcd(n;p) = p ∈ ℤ
11. 0 < gcd(n;p)
⊢ gcd(n;p) = 1 ∈ ℤ

---

Latex:

---

Latex:

1.  p  :  \mBbbN{}
2.  prime(p)
3.  n  :  \{1..p\msupminus{}\}
4.  \mneg{}(p  =  0)
5.  \mneg{}(p  \msim{}  1)
6.  \mforall{}a:\mBbbZ{}.  ((a  |  p)  {}\mRightarrow{}  ((a  \msim{}  1)  \mvee{}  (a  \msim{}  p)))
7.  gcd(n;p)  |  n
8.  gcd(n;p)  |  p
9.  \mforall{}z:\mBbbZ{}.  (((z  |  n)  \mwedge{}  (z  |  p))  {}\mRightarrow{}  (z  |  gcd(n;p)))
\mvdash{}  gcd(n;p)  =  1


By

---

Latex:
((FHyp  6  [-2]  THEN  Auto)
  THEN  RWO  "assoced\_elim"  (-1)
  THEN  Auto
  THEN  InstLemma  `gcd-positive`  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  SplitOrHyps
  THEN  Auto')

---

Home Index