Metamath Proof Explorer

Theorem eulerth

Description: Euler's theorem, a generalization of Fermat's little theorem. If A and N are coprime, then A ^ phi ( N ) == 1 (mod N ). This is Metamath 100 proof #10. Also called Euler-Fermat theorem, see theorem 5.17 in ApostolNT p. 113. (Contributed by Mario Carneiro, 28-Feb-2014)

Ref Expression
Assertion eulerth 
|- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( A ^ ( phi ` N ) ) mod N ) = ( 1 mod N ) )

Proof

Step Hyp Ref Expression
1 phicl 
 |-  ( N e. NN -> ( phi ` N ) e. NN )
2 1 nnnn0d 
 |-  ( N e. NN -> ( phi ` N ) e. NN0 )
3 hashfz1 
 |-  ( ( phi ` N ) e. NN0 -> ( # ` ( 1 ... ( phi ` N ) ) ) = ( phi ` N ) )
4 2 3 syl 
 |-  ( N e. NN -> ( # ` ( 1 ... ( phi ` N ) ) ) = ( phi ` N ) )
5 dfphi2 
 |-  ( N e. NN -> ( phi ` N ) = ( # ` { k e. ( 0 ..^ N ) | ( k gcd N ) = 1 } ) )
6 4 5 eqtrd 
 |-  ( N e. NN -> ( # ` ( 1 ... ( phi ` N ) ) ) = ( # ` { k e. ( 0 ..^ N ) | ( k gcd N ) = 1 } ) )
7 6 3ad2ant1 
 |-  ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( # ` ( 1 ... ( phi ` N ) ) ) = ( # ` { k e. ( 0 ..^ N ) | ( k gcd N ) = 1 } ) )
8 fzfi 
 |-  ( 1 ... ( phi ` N ) ) e. Fin
9 fzofi 
 |-  ( 0 ..^ N ) e. Fin
10 ssrab2 
 |-  { k e. ( 0 ..^ N ) | ( k gcd N ) = 1 } C_ ( 0 ..^ N )
11 ssfi 
 |-  ( ( ( 0 ..^ N ) e. Fin /\ { k e. ( 0 ..^ N ) | ( k gcd N ) = 1 } C_ ( 0 ..^ N ) ) -> { k e. ( 0 ..^ N ) | ( k gcd N ) = 1 } e. Fin )
12 9 10 11 mp2an 
 |-  { k e. ( 0 ..^ N ) | ( k gcd N ) = 1 } e. Fin
13 hashen 
 |-  ( ( ( 1 ... ( phi ` N ) ) e. Fin /\ { k e. ( 0 ..^ N ) | ( k gcd N ) = 1 } e. Fin ) -> ( ( # ` ( 1 ... ( phi ` N ) ) ) = ( # ` { k e. ( 0 ..^ N ) | ( k gcd N ) = 1 } ) <-> ( 1 ... ( phi ` N ) ) ~~ { k e. ( 0 ..^ N ) | ( k gcd N ) = 1 } ) )
14 8 12 13 mp2an 
 |-  ( ( # ` ( 1 ... ( phi ` N ) ) ) = ( # ` { k e. ( 0 ..^ N ) | ( k gcd N ) = 1 } ) <-> ( 1 ... ( phi ` N ) ) ~~ { k e. ( 0 ..^ N ) | ( k gcd N ) = 1 } )
15 7 14 sylib 
 |-  ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( 1 ... ( phi ` N ) ) ~~ { k e. ( 0 ..^ N ) | ( k gcd N ) = 1 } )
16 bren 
 |-  ( ( 1 ... ( phi ` N ) ) ~~ { k e. ( 0 ..^ N ) | ( k gcd N ) = 1 } <-> E. f f : ( 1 ... ( phi ` N ) ) -1-1-onto-> { k e. ( 0 ..^ N ) | ( k gcd N ) = 1 } )
17 15 16 sylib 
 |-  ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> E. f f : ( 1 ... ( phi ` N ) ) -1-1-onto-> { k e. ( 0 ..^ N ) | ( k gcd N ) = 1 } )
18 simpl 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ f : ( 1 ... ( phi ` N ) ) -1-1-onto-> { k e. ( 0 ..^ N ) | ( k gcd N ) = 1 } ) -> ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) )
19 oveq1 
 |-  ( k = y -> ( k gcd N ) = ( y gcd N ) )
20 19 eqeq1d 
 |-  ( k = y -> ( ( k gcd N ) = 1 <-> ( y gcd N ) = 1 ) )
21 20 cbvrabv 
 |-  { k e. ( 0 ..^ N ) | ( k gcd N ) = 1 } = { y e. ( 0 ..^ N ) | ( y gcd N ) = 1 }
22 eqid 
 |-  ( 1 ... ( phi ` N ) ) = ( 1 ... ( phi ` N ) )
23 simpr 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ f : ( 1 ... ( phi ` N ) ) -1-1-onto-> { k e. ( 0 ..^ N ) | ( k gcd N ) = 1 } ) -> f : ( 1 ... ( phi ` N ) ) -1-1-onto-> { k e. ( 0 ..^ N ) | ( k gcd N ) = 1 } )
24 fveq2 
 |-  ( k = x -> ( f ` k ) = ( f ` x ) )
25 24 oveq2d 
 |-  ( k = x -> ( A x. ( f ` k ) ) = ( A x. ( f ` x ) ) )
26 25 oveq1d 
 |-  ( k = x -> ( ( A x. ( f ` k ) ) mod N ) = ( ( A x. ( f ` x ) ) mod N ) )
27 26 cbvmptv 
 |-  ( k e. ( 1 ... ( phi ` N ) ) |-> ( ( A x. ( f ` k ) ) mod N ) ) = ( x e. ( 1 ... ( phi ` N ) ) |-> ( ( A x. ( f ` x ) ) mod N ) )
28 18 21 22 23 27 eulerthlem2 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ f : ( 1 ... ( phi ` N ) ) -1-1-onto-> { k e. ( 0 ..^ N ) | ( k gcd N ) = 1 } ) -> ( ( A ^ ( phi ` N ) ) mod N ) = ( 1 mod N ) )
29 17 28 exlimddv 
 |-  ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( A ^ ( phi ` N ) ) mod N ) = ( 1 mod N ) )