---

Step * 1 of Lemma residues-mod_wf


1. n : ℕ
⊢ filter(λi.(gcd(n;i) =z 1);upto(n)) ∈ residue(n) List
BY
{ (SubsumeC ⌜{x:ℕn| ↑((λi.(gcd(n;i) =z 1)) x)}  List⌝⋅
   THEN Try ((BLemma `filter_type` THEN Auto))
   THEN Reduce 0
   THEN SubtypeReasoning1
   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)
⊢ {x:ℕn| ↑(gcd(n;x) =z 1)}  ⊆r residue(n)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
\mvdash{}  filter(\mlambda{}i.(gcd(n;i)  =\msubz{}  1);upto(n))  \mmember{}  residue(n)  List


By

---

Latex:
(SubsumeC  \mkleeneopen{}\{x:\mBbbN{}n|  \muparrow{}((\mlambda{}i.(gcd(n;i)  =\msubz{}  1))  x)\}    List\mkleeneclose{}\mcdot{}
  THEN  Try  ((BLemma  `filter\_type`  THEN  Auto))
  THEN  Reduce  0
  THEN  SubtypeReasoning1
  THEN  Auto)

---

Home Index