---

Step * 1 1 1 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 ∈ ℤ
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
BY
{ (Thin (-1)
   THEN (GenConcl ⌜1 = M ∈ ℤ⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN MoveToConcl (-1)
   THEN ListInd (-1)
   THEN Reduce 0
   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. u : {x:ℤ| CoPrime(n,x)} 
7. v : {x:ℤ| CoPrime(n,x)}  List
8. ∀M:ℤ
     ((accumulate (with value c and list item x):
        x * c
       over list:
         v
       with starting value:
        M)
     * a^||v||) ≡ accumulate (with value c and list item x):
                   (ax mod n) * c
                  over list:
                    v
                  with starting value:
                   M) mod n)
9. M : ℤ
⊢ (accumulate (with value c and list item x):
    x * c
   over list:
     v
   with starting value:
    u * M)
* a^(||v|| + 1)) ≡ accumulate (with value c and list item x):
                    (ax mod n) * c
                   over list:
                     v
                   with starting value:
                    (au mod n) * M) 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
6.  L  :  \{x:\mBbbZ{}|  CoPrime(n,x)\}    List
7.  residues-mod(n)  =  L
\mvdash{}  (accumulate  (with  value  c  and  list  item  x):
        x  *  c
      over  list:
          L
      with  starting  value:
        1)
*  a\^{}||L||)  \mequiv{}  accumulate  (with  value  c  and  list  item  x):
                            (ax  mod  n)  *  c
                          over  list:
                              L
                          with  starting  value:
                            1)  mod  n


By

---

Latex:
(Thin  (-1)
  THEN  (GenConcl  \mkleeneopen{}1  =  M\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  MoveToConcl  (-1)
  THEN  ListInd  (-1)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index