---

Step * 1 1 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. 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):
                     x * c
                    over list:
                      v
                    with starting value:
                     (au mod n) * M)
* a^||v||) mod n
BY
{ (Thin (-2)
   THEN Assert ⌜accumulate (with value c and list item x):
                 x * c
                over list:
                  v
                with starting value:
                 (au mod n) * M) ≡ (accumulate (with value c and list item x):
                                     x * c
                                    over list:
                                      v
                                    with starting value:
                                     u * M)
                * a) 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 ∈ ℤ
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:
   (au mod n) * M) ≡ (accumulate (with value c and list item x):
                       x * c
                      over list:
                        v
                      with starting value:
                       u * M)
* a) 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. u : {x:ℤ| CoPrime(n,x)} 
7. v : {x:ℤ| CoPrime(n,x)}  List
8. M : ℤ
9. accumulate (with value c and list item x):
    x * c
   over list:
     v
   with starting value:
    (au mod n) * M) ≡ (accumulate (with value c and list item x):
                        x * c
                       over list:
                         v
                       with starting value:
                        u * M)
* a) mod n
⊢ (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):
                     x * c
                    over list:
                      v
                    with starting value:
                     (au mod n) * M)
* a^||v||) 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.  u  :  \{x:\mBbbZ{}|  CoPrime(n,x)\} 
7.  v  :  \{x:\mBbbZ{}|  CoPrime(n,x)\}    List
8.  \mforall{}M:\mBbbZ{}
          ((accumulate  (with  value  c  and  list  item  x):
                x  *  c
              over  list:
                  v
              with  starting  value:
                M)
          *  a\^{}||v||)  \mequiv{}  accumulate  (with  value  c  and  list  item  x):
                                      (ax  mod  n)  *  c
                                    over  list:
                                        v
                                    with  starting  value:
                                      M)  mod  n)
9.  M  :  \mBbbZ{}
\mvdash{}  (accumulate  (with  value  c  and  list  item  x):
        x  *  c
      over  list:
          v
      with  starting  value:
        u  *  M)
*  a\^{}(||v||  +  1))  \mequiv{}  (accumulate  (with  value  c  and  list  item  x):
                                          x  *  c
                                        over  list:
                                            v
                                        with  starting  value:
                                          (au  mod  n)  *  M)
*  a\^{}||v||)  mod  n


By

---

Latex:
(Thin  (-2)
  THEN  Assert  \mkleeneopen{}accumulate  (with  value  c  and  list  item  x):
                              x  *  c
                            over  list:
                                v
                            with  starting  value:
                              (au  mod  n)  *  M)  \mequiv{}  (accumulate  (with  value  c  and  list  item  x):
                                                                      x  *  c
                                                                    over  list:
                                                                        v
                                                                    with  starting  value:
                                                                      u  *  M)
                            *  a)  mod  n\mkleeneclose{}\mcdot{}
  )

---

Home Index