This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem znrrg

Description: The regular elements of Z/nZ are exactly the units. (This theorem fails for N = 0 , where all nonzero integers are regular, but only +- 1 are units.) (Contributed by Mario Carneiro, 18-Apr-2016)

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

Proof

Step Hyp Ref Expression
1 znchr.y 
 |-  Y = ( Z/nZ ` N )
2 znunit.u 
 |-  U = ( Unit ` Y )
3 znrrg.e 
 |-  E = ( RLReg ` Y )
4 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
5 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
6 eqid 
 |-  ( ZRHom ` Y ) = ( ZRHom ` Y )
7 1 5 6 znzrhfo 
 |-  ( N e. NN0 -> ( ZRHom ` Y ) : ZZ -onto-> ( Base ` Y ) )
8 4 7 syl 
 |-  ( N e. NN -> ( ZRHom ` Y ) : ZZ -onto-> ( Base ` Y ) )
9 3 5 rrgss 
 |-  E C_ ( Base ` Y )
10 9 sseli 
 |-  ( x e. E -> x e. ( Base ` Y ) )
11 foelrn 
 |-  ( ( ( ZRHom ` Y ) : ZZ -onto-> ( Base ` Y ) /\ x e. ( Base ` Y ) ) -> E. n e. ZZ x = ( ( ZRHom ` Y ) ` n ) )
12 8 10 11 syl2an 
 |-  ( ( N e. NN /\ x e. E ) -> E. n e. ZZ x = ( ( ZRHom ` Y ) ` n ) )
13 12 ex 
 |-  ( N e. NN -> ( x e. E -> E. n e. ZZ x = ( ( ZRHom ` Y ) ` n ) ) )
14 nncn 
 |-  ( N e. NN -> N e. CC )
15 14 ad2antrr 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> N e. CC )
16 simplr 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> n e. ZZ )
17 nnz 
 |-  ( N e. NN -> N e. ZZ )
18 17 ad2antrr 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> N e. ZZ )
19 nnne0 
 |-  ( N e. NN -> N =/= 0 )
20 19 ad2antrr 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> N =/= 0 )
21 simpr 
 |-  ( ( n = 0 /\ N = 0 ) -> N = 0 )
22 21 necon3ai 
 |-  ( N =/= 0 -> -. ( n = 0 /\ N = 0 ) )
23 20 22 syl 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> -. ( n = 0 /\ N = 0 ) )
24 gcdn0cl 
 |-  ( ( ( n e. ZZ /\ N e. ZZ ) /\ -. ( n = 0 /\ N = 0 ) ) -> ( n gcd N ) e. NN )
25 16 18 23 24 syl21anc 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( n gcd N ) e. NN )
26 25 nncnd 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( n gcd N ) e. CC )
27 25 nnne0d 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( n gcd N ) =/= 0 )
28 15 26 27 divcan2d 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( ( n gcd N ) x. ( N / ( n gcd N ) ) ) = N )
29 gcddvds 
 |-  ( ( n e. ZZ /\ N e. ZZ ) -> ( ( n gcd N ) || n /\ ( n gcd N ) || N ) )
30 16 18 29 syl2anc 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( ( n gcd N ) || n /\ ( n gcd N ) || N ) )
31 30 simpld 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( n gcd N ) || n )
32 25 nnzd 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( n gcd N ) e. ZZ )
33 30 simprd 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( n gcd N ) || N )
34 simpll 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> N e. NN )
35 nndivdvds 
 |-  ( ( N e. NN /\ ( n gcd N ) e. NN ) -> ( ( n gcd N ) || N <-> ( N / ( n gcd N ) ) e. NN ) )
36 34 25 35 syl2anc 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( ( n gcd N ) || N <-> ( N / ( n gcd N ) ) e. NN ) )
37 33 36 mpbid 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( N / ( n gcd N ) ) e. NN )
38 37 nnzd 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( N / ( n gcd N ) ) e. ZZ )
39 dvdsmulc 
 |-  ( ( ( n gcd N ) e. ZZ /\ n e. ZZ /\ ( N / ( n gcd N ) ) e. ZZ ) -> ( ( n gcd N ) || n -> ( ( n gcd N ) x. ( N / ( n gcd N ) ) ) || ( n x. ( N / ( n gcd N ) ) ) ) )
40 32 16 38 39 syl3anc 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( ( n gcd N ) || n -> ( ( n gcd N ) x. ( N / ( n gcd N ) ) ) || ( n x. ( N / ( n gcd N ) ) ) ) )
41 31 40 mpd 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( ( n gcd N ) x. ( N / ( n gcd N ) ) ) || ( n x. ( N / ( n gcd N ) ) ) )
42 28 41 eqbrtrrd 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> N || ( n x. ( N / ( n gcd N ) ) ) )
43 simpr 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( ( ZRHom ` Y ) ` n ) e. E )
44 4 ad2antrr 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> N e. NN0 )
45 44 7 syl 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( ZRHom ` Y ) : ZZ -onto-> ( Base ` Y ) )
46 fof 
 |-  ( ( ZRHom ` Y ) : ZZ -onto-> ( Base ` Y ) -> ( ZRHom ` Y ) : ZZ --> ( Base ` Y ) )
47 45 46 syl 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( ZRHom ` Y ) : ZZ --> ( Base ` Y ) )
48 47 38 ffvelcdmd 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( ( ZRHom ` Y ) ` ( N / ( n gcd N ) ) ) e. ( Base ` Y ) )
49 eqid 
 |-  ( .r ` Y ) = ( .r ` Y )
50 eqid 
 |-  ( 0g ` Y ) = ( 0g ` Y )
51 3 5 49 50 rrgeq0i 
 |-  ( ( ( ( ZRHom ` Y ) ` n ) e. E /\ ( ( ZRHom ` Y ) ` ( N / ( n gcd N ) ) ) e. ( Base ` Y ) ) -> ( ( ( ( ZRHom ` Y ) ` n ) ( .r ` Y ) ( ( ZRHom ` Y ) ` ( N / ( n gcd N ) ) ) ) = ( 0g ` Y ) -> ( ( ZRHom ` Y ) ` ( N / ( n gcd N ) ) ) = ( 0g ` Y ) ) )
52 43 48 51 syl2anc 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( ( ( ( ZRHom ` Y ) ` n ) ( .r ` Y ) ( ( ZRHom ` Y ) ` ( N / ( n gcd N ) ) ) ) = ( 0g ` Y ) -> ( ( ZRHom ` Y ) ` ( N / ( n gcd N ) ) ) = ( 0g ` Y ) ) )
53 1 zncrng 
 |-  ( N e. NN0 -> Y e. CRing )
54 4 53 syl 
 |-  ( N e. NN -> Y e. CRing )
55 crngring 
 |-  ( Y e. CRing -> Y e. Ring )
56 54 55 syl 
 |-  ( N e. NN -> Y e. Ring )
57 56 ad2antrr 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> Y e. Ring )
58 6 zrhrhm 
 |-  ( Y e. Ring -> ( ZRHom ` Y ) e. ( ZZring RingHom Y ) )
59 57 58 syl 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( ZRHom ` Y ) e. ( ZZring RingHom Y ) )
60 zringbas 
 |-  ZZ = ( Base ` ZZring )
61 zringmulr 
 |-  x. = ( .r ` ZZring )
62 60 61 49 rhmmul 
 |-  ( ( ( ZRHom ` Y ) e. ( ZZring RingHom Y ) /\ n e. ZZ /\ ( N / ( n gcd N ) ) e. ZZ ) -> ( ( ZRHom ` Y ) ` ( n x. ( N / ( n gcd N ) ) ) ) = ( ( ( ZRHom ` Y ) ` n ) ( .r ` Y ) ( ( ZRHom ` Y ) ` ( N / ( n gcd N ) ) ) ) )
63 59 16 38 62 syl3anc 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( ( ZRHom ` Y ) ` ( n x. ( N / ( n gcd N ) ) ) ) = ( ( ( ZRHom ` Y ) ` n ) ( .r ` Y ) ( ( ZRHom ` Y ) ` ( N / ( n gcd N ) ) ) ) )
64 63 eqeq1d 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( ( ( ZRHom ` Y ) ` ( n x. ( N / ( n gcd N ) ) ) ) = ( 0g ` Y ) <-> ( ( ( ZRHom ` Y ) ` n ) ( .r ` Y ) ( ( ZRHom ` Y ) ` ( N / ( n gcd N ) ) ) ) = ( 0g ` Y ) ) )
65 16 38 zmulcld 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( n x. ( N / ( n gcd N ) ) ) e. ZZ )
66 1 6 50 zndvds0 
 |-  ( ( N e. NN0 /\ ( n x. ( N / ( n gcd N ) ) ) e. ZZ ) -> ( ( ( ZRHom ` Y ) ` ( n x. ( N / ( n gcd N ) ) ) ) = ( 0g ` Y ) <-> N || ( n x. ( N / ( n gcd N ) ) ) ) )
67 44 65 66 syl2anc 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( ( ( ZRHom ` Y ) ` ( n x. ( N / ( n gcd N ) ) ) ) = ( 0g ` Y ) <-> N || ( n x. ( N / ( n gcd N ) ) ) ) )
68 64 67 bitr3d 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( ( ( ( ZRHom ` Y ) ` n ) ( .r ` Y ) ( ( ZRHom ` Y ) ` ( N / ( n gcd N ) ) ) ) = ( 0g ` Y ) <-> N || ( n x. ( N / ( n gcd N ) ) ) ) )
69 1 6 50 zndvds0 
 |-  ( ( N e. NN0 /\ ( N / ( n gcd N ) ) e. ZZ ) -> ( ( ( ZRHom ` Y ) ` ( N / ( n gcd N ) ) ) = ( 0g ` Y ) <-> N || ( N / ( n gcd N ) ) ) )
70 44 38 69 syl2anc 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( ( ( ZRHom ` Y ) ` ( N / ( n gcd N ) ) ) = ( 0g ` Y ) <-> N || ( N / ( n gcd N ) ) ) )
71 52 68 70 3imtr3d 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( N || ( n x. ( N / ( n gcd N ) ) ) -> N || ( N / ( n gcd N ) ) ) )
72 42 71 mpd 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> N || ( N / ( n gcd N ) ) )
73 15 26 27 divcan1d 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( ( N / ( n gcd N ) ) x. ( n gcd N ) ) = N )
74 37 nncnd 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( N / ( n gcd N ) ) e. CC )
75 74 mulridd 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( ( N / ( n gcd N ) ) x. 1 ) = ( N / ( n gcd N ) ) )
76 72 73 75 3brtr4d 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( ( N / ( n gcd N ) ) x. ( n gcd N ) ) || ( ( N / ( n gcd N ) ) x. 1 ) )
77 1zzd 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> 1 e. ZZ )
78 37 nnne0d 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( N / ( n gcd N ) ) =/= 0 )
79 dvdscmulr 
 |-  ( ( ( n gcd N ) e. ZZ /\ 1 e. ZZ /\ ( ( N / ( n gcd N ) ) e. ZZ /\ ( N / ( n gcd N ) ) =/= 0 ) ) -> ( ( ( N / ( n gcd N ) ) x. ( n gcd N ) ) || ( ( N / ( n gcd N ) ) x. 1 ) <-> ( n gcd N ) || 1 ) )
80 32 77 38 78 79 syl112anc 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( ( ( N / ( n gcd N ) ) x. ( n gcd N ) ) || ( ( N / ( n gcd N ) ) x. 1 ) <-> ( n gcd N ) || 1 ) )
81 76 80 mpbid 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( n gcd N ) || 1 )
82 16 18 gcdcld 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( n gcd N ) e. NN0 )
83 dvds1 
 |-  ( ( n gcd N ) e. NN0 -> ( ( n gcd N ) || 1 <-> ( n gcd N ) = 1 ) )
84 82 83 syl 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( ( n gcd N ) || 1 <-> ( n gcd N ) = 1 ) )
85 81 84 mpbid 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( n gcd N ) = 1 )
86 1 2 6 znunit 
 |-  ( ( N e. NN0 /\ n e. ZZ ) -> ( ( ( ZRHom ` Y ) ` n ) e. U <-> ( n gcd N ) = 1 ) )
87 44 16 86 syl2anc 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( ( ( ZRHom ` Y ) ` n ) e. U <-> ( n gcd N ) = 1 ) )
88 85 87 mpbird 
 |-  ( ( ( N e. NN /\ n e. ZZ ) /\ ( ( ZRHom ` Y ) ` n ) e. E ) -> ( ( ZRHom ` Y ) ` n ) e. U )
89 88 ex 
 |-  ( ( N e. NN /\ n e. ZZ ) -> ( ( ( ZRHom ` Y ) ` n ) e. E -> ( ( ZRHom ` Y ) ` n ) e. U ) )
90 eleq1 
 |-  ( x = ( ( ZRHom ` Y ) ` n ) -> ( x e. E <-> ( ( ZRHom ` Y ) ` n ) e. E ) )
91 eleq1 
 |-  ( x = ( ( ZRHom ` Y ) ` n ) -> ( x e. U <-> ( ( ZRHom ` Y ) ` n ) e. U ) )
92 90 91 imbi12d 
 |-  ( x = ( ( ZRHom ` Y ) ` n ) -> ( ( x e. E -> x e. U ) <-> ( ( ( ZRHom ` Y ) ` n ) e. E -> ( ( ZRHom ` Y ) ` n ) e. U ) ) )
93 89 92 syl5ibrcom 
 |-  ( ( N e. NN /\ n e. ZZ ) -> ( x = ( ( ZRHom ` Y ) ` n ) -> ( x e. E -> x e. U ) ) )
94 93 rexlimdva 
 |-  ( N e. NN -> ( E. n e. ZZ x = ( ( ZRHom ` Y ) ` n ) -> ( x e. E -> x e. U ) ) )
95 94 com23 
 |-  ( N e. NN -> ( x e. E -> ( E. n e. ZZ x = ( ( ZRHom ` Y ) ` n ) -> x e. U ) ) )
96 13 95 mpdd 
 |-  ( N e. NN -> ( x e. E -> x e. U ) )
97 96 ssrdv 
 |-  ( N e. NN -> E C_ U )
98 3 2 unitrrg 
 |-  ( Y e. Ring -> U C_ E )
99 56 98 syl 
 |-  ( N e. NN -> U C_ E )
100 97 99 eqssd 
 |-  ( N e. NN -> E = U )