---

Step * of Lemma residue-mul_wf

∀[n:ℕ+]. ∀[a,i:ℤ].  (ai mod n) ∈ residue(n) supposing CoPrime(n,a) ∧ CoPrime(n,i)
BY
{ (Unfold `residue` 0
   THEN ProveWfLemma
   THEN (MemTypeCD THEN Auto)
   THEN Try ((BLemma `mod_bounds` THEN Auto))
   THEN BLemma `coprime-mod`
   THEN Auto) }

1
1. n : ℕ+
2. a : ℤ
3. i : ℤ
4. CoPrime(n,a)
5. CoPrime(n,i)
⊢ CoPrime(n,a * i)

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[a,i:\mBbbZ{}].    (ai  mod  n)  \mmember{}  residue(n)  supposing  CoPrime(n,a)  \mwedge{}  CoPrime(n,i)


By

---

Latex:
(Unfold  `residue`  0
  THEN  ProveWfLemma
  THEN  (MemTypeCD  THEN  Auto)
  THEN  Try  ((BLemma  `mod\_bounds`  THEN  Auto))
  THEN  BLemma  `coprime-mod`
  THEN  Auto)

---

Home Index