---

Step * of Lemma gcd-prime

∀[p:ℕ]. ∀[n:{1..p-}]. (gcd(n;p) = 1 ∈ ℤ) supposing prime(p)
BY
{ (Auto
   THEN (InstLemma `prime_elim` [⌜p⌝]⋅ THEN Auto)
   THEN (InstLemma `gcd_sat_gcd_p` [⌜n⌝;⌜p⌝]⋅ THENA Auto)
   THEN D -1
   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)))
⊢ gcd(n;p) = 1 ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[p:\mBbbN{}].  \mforall{}[n:\{1..p\msupminus{}\}].  (gcd(n;p)  =  1)  supposing  prime(p)


By

---

Latex:
(Auto
  THEN  (InstLemma  `prime\_elim`  [\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  (InstLemma  `gcd\_sat\_gcd\_p`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  Auto)

---

Home Index