---

Step * 1 of Lemma Euler-Fermat


1. n : {2...}
2. a : ℕ+
3. CoPrime(n,a)
4. Πx ∈ map(λi.(ai mod n);residues-mod(n)). x = Πx ∈ residues-mod(n). x ∈ ℤ
5. Πx ∈ residues-mod(n). (ax mod n) = Πx ∈ residues-mod(n). x ∈ ℤ
⊢ a^totient(n) ≡ 1 mod n
BY
{ Assert ⌜(Πx ∈ residues-mod(n). x * a^totient(n)) ≡ (Πx ∈ residues-mod(n). x * 1) mod n⌝⋅ }

1
.....assertion..... 
1. n : {2...}
2. a : ℕ+
3. CoPrime(n,a)
4. Πx ∈ map(λi.(ai mod n);residues-mod(n)). x = Πx ∈ residues-mod(n). x ∈ ℤ
5. Πx ∈ residues-mod(n). (ax mod n) = Πx ∈ residues-mod(n). x ∈ ℤ
⊢ (Πx ∈ residues-mod(n). x * a^totient(n)) ≡ (Πx ∈ residues-mod(n). x * 1) mod n

2
1. n : {2...}
2. a : ℕ+
3. CoPrime(n,a)
4. Πx ∈ map(λi.(ai mod n);residues-mod(n)). x = Πx ∈ residues-mod(n). x ∈ ℤ
5. Πx ∈ residues-mod(n). (ax mod n) = Πx ∈ residues-mod(n). x ∈ ℤ
6. (Πx ∈ residues-mod(n). x * a^totient(n)) ≡ (Πx ∈ residues-mod(n). x * 1) mod n
⊢ a^totient(n) ≡ 1 mod n

---

Latex:

---

Latex:

1.  n  :  \{2...\}
2.  a  :  \mBbbN{}\msupplus{}
3.  CoPrime(n,a)
4.  \mPi{}x  \mmember{}  map(\mlambda{}i.(ai  mod  n);residues-mod(n)).  x  =  \mPi{}x  \mmember{}  residues-mod(n).  x
5.  \mPi{}x  \mmember{}  residues-mod(n).  (ax  mod  n)  =  \mPi{}x  \mmember{}  residues-mod(n).  x
\mvdash{}  a\^{}totient(n)  \mequiv{}  1  mod  n


By

---

Latex:
Assert  \mkleeneopen{}(\mPi{}x  \mmember{}  residues-mod(n).  x  *  a\^{}totient(n))  \mequiv{}  (\mPi{}x  \mmember{}  residues-mod(n).  x  *  1)  mod  n\mkleeneclose{}\mcdot{}

---

Home Index