---

Step * 1 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)))
10. gcd(n;p) = p ∈ ℤ
11. 0 < gcd(n;p)
⊢ gcd(n;p) = 1 ∈ ℤ
BY
{ (FLemma `divisor_bound` [-5] THEN Auto') }

---

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)))
10.  gcd(n;p)  =  p
11.  0  <  gcd(n;p)
\mvdash{}  gcd(n;p)  =  1


By

---

Latex:
(FLemma  `divisor\_bound`  [-5]  THEN  Auto')

---

Home Index