---

Step * 1 1 of Lemma residues-mod_wf


1. n : ℕ
2. filter(λi.(gcd(n;i) =z 1);upto(n)) = filter(λi.(gcd(n;i) =z 1);upto(n)) ∈ ({x:ℕn| ↑((λi.(gcd(n;i) =z 1)) x)}  List)
⊢ {x:ℕn| ↑(gcd(n;x) =z 1)}  ⊆r residue(n)
BY
{ (Unfold `residue` 0
   THEN (D 0 THENM D -1)
   THEN Auto
   THEN RW assert_pushdownC (-1)
   THEN Auto
   THEN MemTypeCD
   THEN Auto
   THEN BLemma `coprime_elim_a`
   THEN Auto) }

1
1. n : ℕ
2. filter(λi.(gcd(n;i) =z 1);upto(n)) = filter(λi.(gcd(n;i) =z 1);upto(n)) ∈ ({x:ℕn| ↑((λi.(gcd(n;i) =z 1)) x)}  List)
3. x : ℕn@i
4. gcd(n;x) = 1 ∈ ℤ
⊢ gcd(n;x) ~ 1

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  filter(\mlambda{}i.(gcd(n;i)  =\msubz{}  1);upto(n))  =  filter(\mlambda{}i.(gcd(n;i)  =\msubz{}  1);upto(n))
\mvdash{}  \{x:\mBbbN{}n|  \muparrow{}(gcd(n;x)  =\msubz{}  1)\}    \msubseteq{}r  residue(n)


By

---

Latex:
(Unfold  `residue`  0
  THEN  (D  0  THENM  D  -1)
  THEN  Auto
  THEN  RW  assert\_pushdownC  (-1)
  THEN  Auto
  THEN  MemTypeCD
  THEN  Auto
  THEN  BLemma  `coprime\_elim\_a`
  THEN  Auto)

---

Home Index