---

Step * of Lemma residues-permute

∀n:{2...}. ∀a:ℕ+.  (CoPrime(n,a) ⇒ permutation(residue(n);map(λi.(ai mod n);residues-mod(n));residues-mod(n)))
BY
{ xxx(Auto
      THEN (InstLemma `residue-mul-inverse` [⌜n⌝;⌜a⌝]⋅ THENA Auto)
      THEN ExRepD
      THEN (BLemma `permutation-when-no_repeats`
            THEN Auto
            THEN Try ((BLemma `no_repeats-residues-mod`⋅ THEN Auto))
            THEN Try ((DVar `i' THEN Unhide THEN Auto))
            THEN Try ((BLemma `member-residues-mod`⋅ THEN Auto)))⋅)xxx }

1
1. n : {2...}
2. a : ℕ+
3. CoPrime(n,a)
4. b : ℤ
5. CoPrime(n,b)
6. ∀i:residue(n)
     ((((ba mod n) = 1 ∈ residue(n)) ∧ ((ab mod n) = 1 ∈ residue(n)))
     ∧ ((b(ai mod n) mod n) = i ∈ residue(n))
     ∧ ((a(bi mod n) mod n) = i ∈ residue(n)))
7. x : residue(n)
8. (x ∈ residues-mod(n))
⊢ (x ∈ map(λi.(ai mod n);residues-mod(n)))

2
1. n : {2...}
2. a : ℕ+
3. CoPrime(n,a)
4. b : ℤ
5. CoPrime(n,b)
6. ∀i:residue(n)
     ((((ba mod n) = 1 ∈ residue(n)) ∧ ((ab mod n) = 1 ∈ residue(n)))
     ∧ ((b(ai mod n) mod n) = i ∈ residue(n))
     ∧ ((a(bi mod n) mod n) = i ∈ residue(n)))
⊢ no_repeats(residue(n);map(λi.(ai mod n);residues-mod(n)))

---

Latex:

---

Latex:
\mforall{}n:\{2...\}.  \mforall{}a:\mBbbN{}\msupplus{}.
    (CoPrime(n,a)  {}\mRightarrow{}  permutation(residue(n);map(\mlambda{}i.(ai  mod  n);residues-mod(n));residues-mod(n)))


By

---

Latex:
xxx(Auto
        THEN  (InstLemma  `residue-mul-inverse`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)
        THEN  ExRepD
        THEN  (BLemma  `permutation-when-no\_repeats`
                    THEN  Auto
                    THEN  Try  ((BLemma  `no\_repeats-residues-mod`\mcdot{}  THEN  Auto))
                    THEN  Try  ((DVar  `i'  THEN  Unhide  THEN  Auto))
                    THEN  Try  ((BLemma  `member-residues-mod`\mcdot{}  THEN  Auto)))\mcdot{})xxx

---

Home Index