---

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


1. n : {2...}
2. u : {x:ℤ| CoPrime(n,x)} 
3. v : {x:ℤ| CoPrime(n,x)}  List
⊢ accumulate (with value c and list item x):
   x * c
  over list:
    v
  with starting value:
   u * 1) ~ u * accumulate (with value c and list item x): x * cover list:  vwith starting value: 1)
BY
{ ((D -2 THEN Thin (-2))
   THEN MoveToConcl (-2)
   THEN ListInd (-1)
   THEN Reduce 0
   THEN Auto
   THEN Subst' u * u@0 * 1 ~ (u * u@0) * 1 0
   THEN Auto
   THEN RWO "-2" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \{2...\}
2.  u  :  \{x:\mBbbZ{}|  CoPrime(n,x)\} 
3.  v  :  \{x:\mBbbZ{}|  CoPrime(n,x)\}    List
\mvdash{}  accumulate  (with  value  c  and  list  item  x):
      x  *  c
    over  list:
        v
    with  starting  value:
      u  *  1)  \msim{}  u  *  accumulate  (with  value  c  and  list  item  x):  x  *  cover  list:    vwith  starting  value:  1)


By

---

Latex:
((D  -2  THEN  Thin  (-2))
  THEN  MoveToConcl  (-2)
  THEN  ListInd  (-1)
  THEN  Reduce  0
  THEN  Auto
  THEN  Subst'  u  *  u@0  *  1  \msim{}  (u  *  u@0)  *  1  0
  THEN  Auto
  THEN  RWO  "-2"  0
  THEN  Auto)

---

Home Index