---

Step * 1 1 1 of Lemma Euler-Fermat

.....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). (ax mod n) mod n
BY
{ (RepUR ``bag-product bag-summation bag-accum totient`` 0⋅
   THEN (GenConcl ⌜residues-mod(n) = L ∈ ({x:ℤ| CoPrime(n,x)}  List)⌝⋅ THENA (Auto THEN DVar `u' THEN Unhide THEN Auto))
   ) }

1
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. L : {x:ℤ| CoPrime(n,x)}  List
7. residues-mod(n) = L ∈ ({x:ℤ| CoPrime(n,x)}  List)
⊢ (accumulate (with value c and list item x):
    x * c
   over list:
     L
   with starting value:
    1)
* a^||L||) ≡ accumulate (with value c and list item x):
              (ax mod n) * c
             over list:
               L
             with starting value:
              1) mod n

---

Latex:

---

Latex:
.....assertion..... 
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{}  (\mPi{}x  \mmember{}  residues-mod(n).  x  *  a\^{}totient(n))  \mequiv{}  \mPi{}x  \mmember{}  residues-mod(n).  (ax  mod  n)  mod  n


By

---

Latex:
(RepUR  ``bag-product  bag-summation  bag-accum  totient``  0\mcdot{}
  THEN  (GenConcl  \mkleeneopen{}residues-mod(n)  =  L\mkleeneclose{}\mcdot{}  THENA  (Auto  THEN  DVar  `u'  THEN  Unhide  THEN  Auto))
  )

---

Home Index