This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
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 ) ) |
| 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 | eqabdv | |- ( 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 ) ) |