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