---

Step * 2 1 of Lemma member-residues-mod


1. n : ℕ
2. x : ℕn
3. CoPrime(n,x)
4. filter(λi.(gcd(n;i) =z 1);upto(n)) ∈ {k:ℕn| CoPrime(n,k)}  List
5. (x ∈ upto(n))
⊢ gcd(n;x) = 1 ∈ ℤ
BY
{ (Thin (-1)
   THEN ((FLemma `coprime_elim_a` [-2] THEN Auto)
         THEN RWO "assoced_nelim" (-1)
         THEN Auto
         THEN BLemma `gcd-non-neg`
         THEN Auto)⋅
   ) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  x  :  \mBbbN{}n
3.  CoPrime(n,x)
4.  filter(\mlambda{}i.(gcd(n;i)  =\msubz{}  1);upto(n))  \mmember{}  \{k:\mBbbN{}n|  CoPrime(n,k)\}    List
5.  (x  \mmember{}  upto(n))
\mvdash{}  gcd(n;x)  =  1


By

---

Latex:
(Thin  (-1)
  THEN  ((FLemma  `coprime\_elim\_a`  [-2]  THEN  Auto)
              THEN  RWO  "assoced\_nelim"  (-1)
              THEN  Auto
              THEN  BLemma  `gcd-non-neg`
              THEN  Auto)\mcdot{}
  )

---

Home Index