Metamath Proof Explorer

Theorem znunithash

Description: The size of the unit group of Z/nZ . (Contributed by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses znchr.y 
|- Y = ( Z/nZ ` N )
znunit.u 
|- U = ( Unit ` Y )
Assertion znunithash 
|- ( N e. NN -> ( # ` U ) = ( phi ` N ) )

Proof

Step Hyp Ref Expression
1 znchr.y 
 |-  Y = ( Z/nZ ` N )
2 znunit.u 
 |-  U = ( Unit ` Y )
3 dfphi2 
 |-  ( N e. NN -> ( phi ` N ) = ( # ` { x e. ( 0 ..^ N ) | ( x gcd N ) = 1 } ) )
4 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
5 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
6 eqid 
 |-  ( ( ZRHom ` Y ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) = ( ( ZRHom ` Y ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) )
7 eqid 
 |-  if ( N = 0 , ZZ , ( 0 ..^ N ) ) = if ( N = 0 , ZZ , ( 0 ..^ N ) )
8 1 5 6 7 znf1o 
 |-  ( N e. NN0 -> ( ( ZRHom ` Y ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) : if ( N = 0 , ZZ , ( 0 ..^ N ) ) -1-1-onto-> ( Base ` Y ) )
9 4 8 syl 
 |-  ( N e. NN -> ( ( ZRHom ` Y ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) : if ( N = 0 , ZZ , ( 0 ..^ N ) ) -1-1-onto-> ( Base ` Y ) )
10 nnne0 
 |-  ( N e. NN -> N =/= 0 )
11 ifnefalse 
 |-  ( N =/= 0 -> if ( N = 0 , ZZ , ( 0 ..^ N ) ) = ( 0 ..^ N ) )
12 reseq2 
 |-  ( if ( N = 0 , ZZ , ( 0 ..^ N ) ) = ( 0 ..^ N ) -> ( ( ZRHom ` Y ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) = ( ( ZRHom ` Y ) |` ( 0 ..^ N ) ) )
13 12 f1oeq1d 
 |-  ( if ( N = 0 , ZZ , ( 0 ..^ N ) ) = ( 0 ..^ N ) -> ( ( ( ZRHom ` Y ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) : if ( N = 0 , ZZ , ( 0 ..^ N ) ) -1-1-onto-> ( Base ` Y ) <-> ( ( ZRHom ` Y ) |` ( 0 ..^ N ) ) : if ( N = 0 , ZZ , ( 0 ..^ N ) ) -1-1-onto-> ( Base ` Y ) ) )
14 f1oeq2 
 |-  ( if ( N = 0 , ZZ , ( 0 ..^ N ) ) = ( 0 ..^ N ) -> ( ( ( ZRHom ` Y ) |` ( 0 ..^ N ) ) : if ( N = 0 , ZZ , ( 0 ..^ N ) ) -1-1-onto-> ( Base ` Y ) <-> ( ( ZRHom ` Y ) |` ( 0 ..^ N ) ) : ( 0 ..^ N ) -1-1-onto-> ( Base ` Y ) ) )
15 13 14 bitrd 
 |-  ( if ( N = 0 , ZZ , ( 0 ..^ N ) ) = ( 0 ..^ N ) -> ( ( ( ZRHom ` Y ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) : if ( N = 0 , ZZ , ( 0 ..^ N ) ) -1-1-onto-> ( Base ` Y ) <-> ( ( ZRHom ` Y ) |` ( 0 ..^ N ) ) : ( 0 ..^ N ) -1-1-onto-> ( Base ` Y ) ) )
16 10 11 15 3syl 
 |-  ( N e. NN -> ( ( ( ZRHom ` Y ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) : if ( N = 0 , ZZ , ( 0 ..^ N ) ) -1-1-onto-> ( Base ` Y ) <-> ( ( ZRHom ` Y ) |` ( 0 ..^ N ) ) : ( 0 ..^ N ) -1-1-onto-> ( Base ` Y ) ) )
17 9 16 mpbid 
 |-  ( N e. NN -> ( ( ZRHom ` Y ) |` ( 0 ..^ N ) ) : ( 0 ..^ N ) -1-1-onto-> ( Base ` Y ) )
18 f1ofn 
 |-  ( ( ( ZRHom ` Y ) |` ( 0 ..^ N ) ) : ( 0 ..^ N ) -1-1-onto-> ( Base ` Y ) -> ( ( ZRHom ` Y ) |` ( 0 ..^ N ) ) Fn ( 0 ..^ N ) )
19 elpreima 
 |-  ( ( ( ZRHom ` Y ) |` ( 0 ..^ N ) ) Fn ( 0 ..^ N ) -> ( x e. ( `' ( ( ZRHom ` Y ) |` ( 0 ..^ N ) ) " U ) <-> ( x e. ( 0 ..^ N ) /\ ( ( ( ZRHom ` Y ) |` ( 0 ..^ N ) ) ` x ) e. U ) ) )
20 17 18 19 3syl 
 |-  ( N e. NN -> ( x e. ( `' ( ( ZRHom ` Y ) |` ( 0 ..^ N ) ) " U ) <-> ( x e. ( 0 ..^ N ) /\ ( ( ( ZRHom ` Y ) |` ( 0 ..^ N ) ) ` x ) e. U ) ) )
21 fvres 
 |-  ( x e. ( 0 ..^ N ) -> ( ( ( ZRHom ` Y ) |` ( 0 ..^ N ) ) ` x ) = ( ( ZRHom ` Y ) ` x ) )
22 21 adantl 
 |-  ( ( N e. NN /\ x e. ( 0 ..^ N ) ) -> ( ( ( ZRHom ` Y ) |` ( 0 ..^ N ) ) ` x ) = ( ( ZRHom ` Y ) ` x ) )
23 22 eleq1d 
 |-  ( ( N e. NN /\ x e. ( 0 ..^ N ) ) -> ( ( ( ( ZRHom ` Y ) |` ( 0 ..^ N ) ) ` x ) e. U <-> ( ( ZRHom ` Y ) ` x ) e. U ) )
24 elfzoelz 
 |-  ( x e. ( 0 ..^ N ) -> x e. ZZ )
25 eqid 
 |-  ( ZRHom ` Y ) = ( ZRHom ` Y )
26 1 2 25 znunit 
 |-  ( ( N e. NN0 /\ x e. ZZ ) -> ( ( ( ZRHom ` Y ) ` x ) e. U <-> ( x gcd N ) = 1 ) )
27 4 24 26 syl2an 
 |-  ( ( N e. NN /\ x e. ( 0 ..^ N ) ) -> ( ( ( ZRHom ` Y ) ` x ) e. U <-> ( x gcd N ) = 1 ) )
28 23 27 bitrd 
 |-  ( ( N e. NN /\ x e. ( 0 ..^ N ) ) -> ( ( ( ( ZRHom ` Y ) |` ( 0 ..^ N ) ) ` x ) e. U <-> ( x gcd N ) = 1 ) )
29 28 pm5.32da 
 |-  ( N e. NN -> ( ( x e. ( 0 ..^ N ) /\ ( ( ( ZRHom ` Y ) |` ( 0 ..^ N ) ) ` x ) e. U ) <-> ( x e. ( 0 ..^ N ) /\ ( x gcd N ) = 1 ) ) )
30 20 29 bitrd 
 |-  ( N e. NN -> ( x e. ( `' ( ( ZRHom ` Y ) |` ( 0 ..^ N ) ) " U ) <-> ( x e. ( 0 ..^ N ) /\ ( x gcd N ) = 1 ) ) )
31 30 abbi2dv 
 |-  ( N e. NN -> ( `' ( ( ZRHom ` Y ) |` ( 0 ..^ N ) ) " U ) = { x | ( x e. ( 0 ..^ N ) /\ ( x gcd N ) = 1 ) } )
32 df-rab 
 |-  { x e. ( 0 ..^ N ) | ( x gcd N ) = 1 } = { x | ( x e. ( 0 ..^ N ) /\ ( x gcd N ) = 1 ) }
33 31 32 eqtr4di 
 |-  ( N e. NN -> ( `' ( ( ZRHom ` Y ) |` ( 0 ..^ N ) ) " U ) = { x e. ( 0 ..^ N ) | ( x gcd N ) = 1 } )
34 33 fveq2d 
 |-  ( N e. NN -> ( # ` ( `' ( ( ZRHom ` Y ) |` ( 0 ..^ N ) ) " U ) ) = ( # ` { x e. ( 0 ..^ N ) | ( x gcd N ) = 1 } ) )
35 f1ocnv 
 |-  ( ( ( ZRHom ` Y ) |` ( 0 ..^ N ) ) : ( 0 ..^ N ) -1-1-onto-> ( Base ` Y ) -> `' ( ( ZRHom ` Y ) |` ( 0 ..^ N ) ) : ( Base ` Y ) -1-1-onto-> ( 0 ..^ N ) )
36 f1of1 
 |-  ( `' ( ( ZRHom ` Y ) |` ( 0 ..^ N ) ) : ( Base ` Y ) -1-1-onto-> ( 0 ..^ N ) -> `' ( ( ZRHom ` Y ) |` ( 0 ..^ N ) ) : ( Base ` Y ) -1-1-> ( 0 ..^ N ) )
37 17 35 36 3syl 
 |-  ( N e. NN -> `' ( ( ZRHom ` Y ) |` ( 0 ..^ N ) ) : ( Base ` Y ) -1-1-> ( 0 ..^ N ) )
38 ovexd 
 |-  ( N e. NN -> ( 0 ..^ N ) e. _V )
39 5 2 unitss 
 |-  U C_ ( Base ` Y )
40 39 a1i 
 |-  ( N e. NN -> U C_ ( Base ` Y ) )
41 2 fvexi 
 |-  U e. _V
42 41 a1i 
 |-  ( N e. NN -> U e. _V )
43 f1imaen2g 
 |-  ( ( ( `' ( ( ZRHom ` Y ) |` ( 0 ..^ N ) ) : ( Base ` Y ) -1-1-> ( 0 ..^ N ) /\ ( 0 ..^ N ) e. _V ) /\ ( U C_ ( Base ` Y ) /\ U e. _V ) ) -> ( `' ( ( ZRHom ` Y ) |` ( 0 ..^ N ) ) " U ) ~~ U )
44 37 38 40 42 43 syl22anc 
 |-  ( N e. NN -> ( `' ( ( ZRHom ` Y ) |` ( 0 ..^ N ) ) " U ) ~~ U )
45 hasheni 
 |-  ( ( `' ( ( ZRHom ` Y ) |` ( 0 ..^ N ) ) " U ) ~~ U -> ( # ` ( `' ( ( ZRHom ` Y ) |` ( 0 ..^ N ) ) " U ) ) = ( # ` U ) )
46 44 45 syl 
 |-  ( N e. NN -> ( # ` ( `' ( ( ZRHom ` Y ) |` ( 0 ..^ N ) ) " U ) ) = ( # ` U ) )
47 3 34 46 3eqtr2rd 
 |-  ( N e. NN -> ( # ` U ) = ( phi ` N ) )