---

Step * 1 1 1 1 1 1 1 1 of Lemma Euler-Fermat

.....equality..... 
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 * cover list:  vwith starting value: u * M) * a 
~ accumulate (with value c and list item x):
   x * c
  over list:
    v
  with starting value:
   (u * M) * a)
BY
{ ((GenConcl ⌜(u * M) = N ∈ ℤ⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN MoveToConcl (-1)
   THEN Thin (-1)
   THEN ListInd (-1)
   THEN Reduce 0
   THEN Auto
   THEN RWO "-2" 0
   THEN Auto) }

---

Latex:

---

Latex:
.....equality..... 
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  *  cover  list:    vwith  starting  value:  u  *  M)  *  a 
\msim{}  accumulate  (with  value  c  and  list  item  x):
      x  *  c
    over  list:
        v
    with  starting  value:
      (u  *  M)  *  a)


By

---

Latex:
((GenConcl  \mkleeneopen{}(u  *  M)  =  N\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  MoveToConcl  (-1)
  THEN  Thin  (-1)
  THEN  ListInd  (-1)
  THEN  Reduce  0
  THEN  Auto
  THEN  RWO  "-2"  0
  THEN  Auto)

---

Home Index