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


1. {2...}
2. : ℕ+
3. CoPrime(n,a)
4. Πx ∈ map(λi.(ai mod n);residues-mod(n)). = Πx ∈ residues-mod(n). x ∈ ℤ
5. Πx ∈ residues-mod(n). (ax mod n) = Πx ∈ residues-mod(n). x ∈ ℤ
6. x ∈ residues-mod(n). a^totient(n)) ≡ x ∈ residues-mod(n). 1) mod n
7. {x:ℤCoPrime(n,x)} 
8. {x:ℤCoPrime(n,x)}  List
9. CoPrime(accumulate (with value and list item x): cover list:  vwith starting value: 1),n)
⊢ CoPrime(accumulate (with value and list item x): cover list:  vwith starting value: 1),n)
BY
Subst ⌜accumulate (with value and list item x):
          c
         over list:
           v
         with starting value:
          1) accumulate (with value and list item x): cover list:  vwith starting value: 1)⌝ 0⋅ }

1
.....equality..... 
1. {2...}
2. : ℕ+
3. CoPrime(n,a)
4. Πx ∈ map(λi.(ai mod n);residues-mod(n)). = Πx ∈ residues-mod(n). x ∈ ℤ
5. Πx ∈ residues-mod(n). (ax mod n) = Πx ∈ residues-mod(n). x ∈ ℤ
6. x ∈ residues-mod(n). a^totient(n)) ≡ x ∈ residues-mod(n). 1) mod n
7. {x:ℤCoPrime(n,x)} 
8. {x:ℤCoPrime(n,x)}  List
9. CoPrime(accumulate (with value and list item x): cover list:  vwith starting value: 1),n)
⊢ accumulate (with value and list item x):
   c
  over list:
    v
  with starting value:
   1) accumulate (with value and list item x): cover list:  vwith starting value: 1)

2
1. {2...}
2. : ℕ+
3. CoPrime(n,a)
4. Πx ∈ map(λi.(ai mod n);residues-mod(n)). = Πx ∈ residues-mod(n). x ∈ ℤ
5. Πx ∈ residues-mod(n). (ax mod n) = Πx ∈ residues-mod(n). x ∈ ℤ
6. x ∈ residues-mod(n). a^totient(n)) ≡ x ∈ residues-mod(n). 1) mod n
7. {x:ℤCoPrime(n,x)} 
8. {x:ℤCoPrime(n,x)}  List
9. CoPrime(accumulate (with value and list item x): cover list:  vwith starting value: 1),n)
⊢ CoPrime(u accumulate (with value and list item x): cover list:  vwith starting value: 1),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.  (\mPi{}x  \mmember{}  residues-mod(n).  x  *  a\^{}totient(n))  \mequiv{}  (\mPi{}x  \mmember{}  residues-mod(n).  x  *  1)  mod  n
7.  u  :  \{x:\mBbbZ{}|  CoPrime(n,x)\} 
8.  v  :  \{x:\mBbbZ{}|  CoPrime(n,x)\}    List
9.  CoPrime(accumulate  (with  value  c  and  list  item  x):  x  *  cover  list:    vwith  starting  value:  1),n)
\mvdash{}  CoPrime(accumulate  (with  value  c  and  list  item  x):
                      x  *  c
                    over  list:
                        v
                    with  starting  value:
                      u  *  1)
                  ,n)


By


Latex:
Subst  \mkleeneopen{}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  *  c
                  over  list:
                      v
                  with  starting  value:
                    1)\mkleeneclose{}  0\mcdot{}




Home Index