---

Step * 1 1 1 1 1 1 1 2 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 ∈ ℤ
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))
BY
{ (All Thin
   THEN ListInd (-1)
   THEN Reduce 0
   THEN Auto
   THEN BackThruSomeHyp
   THEN Auto
   THEN RWO "-1" 0
   THEN Auto
   THEN RelRST
   THEN Auto) }

---

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
6.  u  :  \{x:\mBbbZ{}|  CoPrime(n,x)\} 
7.  v  :  \{x:\mBbbZ{}|  CoPrime(n,x)\}    List
8.  M  :  \mBbbZ{}
\mvdash{}  \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))


By

---

Latex:
(All  Thin
  THEN  ListInd  (-1)
  THEN  Reduce  0
  THEN  Auto
  THEN  BackThruSomeHyp
  THEN  Auto
  THEN  RWO  "-1"  0
  THEN  Auto
  THEN  RelRST
  THEN  Auto)

---

Home Index