---

Step * 1 1 1 1 1 1 1 2 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:
   (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
BY
{ Assert ⌜∀a,b:ℤ.
            ((a ≡ b mod n)
            ⇒ (accumulate (with value c and list item x):
                 x * c
                over list:
                  v
                with starting value:
                 a) ≡ accumulate (with value c and list item x):
                       x * c
                      over list:
                        v
                      with starting value:
                       b) 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 : ℤ
⊢ ∀a,b:ℤ.
    ((a ≡ b mod n)
    ⇒ (accumulate (with value c and list item x):
         x * c
        over list:
          v
        with starting value:
         a) ≡ accumulate (with value c and list item x):
               x * c
              over list:
                v
              with starting value:
               b) 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. ∀a,b:ℤ.
     ((a ≡ b mod n)
     ⇒ (accumulate (with value c and list item x):
          x * c
         over list:
           v
         with starting value:
          a) ≡ accumulate (with value c and list item x):
                x * c
               over list:
                 v
               with starting value:
                b) mod n))
⊢ 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

---

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.  M  :  \mBbbZ{}
\mvdash{}  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


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}a,b:\mBbbZ{}.
                    ((a  \mequiv{}  b  mod  n)
                    {}\mRightarrow{}  (accumulate  (with  value  c  and  list  item  x):
                              x  *  c
                            over  list:
                                v
                            with  starting  value:
                              a)  \mequiv{}  accumulate  (with  value  c  and  list  item  x):
                                          x  *  c
                                        over  list:
                                            v
                                        with  starting  value:
                                          b)  mod  n))\mkleeneclose{}\mcdot{}

---

Home Index