Metamath Proof Explorer

Theorem znunit

Description: The units of Z/nZ are the integers coprime to the base. (Contributed by Mario Carneiro, 18-Apr-2016)

Ref Expression
Hypotheses znchr.y 
|- Y = ( Z/nZ ` N )
znunit.u 
|- U = ( Unit ` Y )
znunit.l 
|- L = ( ZRHom ` Y )
Assertion znunit 
|- ( ( N e. NN0 /\ A e. ZZ ) -> ( ( L ` A ) e. U <-> ( A gcd N ) = 1 ) )

Proof

Step Hyp Ref Expression
1 znchr.y 
 |-  Y = ( Z/nZ ` N )
2 znunit.u 
 |-  U = ( Unit ` Y )
3 znunit.l 
 |-  L = ( ZRHom ` Y )
4 1 zncrng 
 |-  ( N e. NN0 -> Y e. CRing )
5 4 adantr 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> Y e. CRing )
6 eqid 
 |-  ( 1r ` Y ) = ( 1r ` Y )
7 eqid 
 |-  ( ||r ` Y ) = ( ||r ` Y )
8 2 6 7 crngunit 
 |-  ( Y e. CRing -> ( ( L ` A ) e. U <-> ( L ` A ) ( ||r ` Y ) ( 1r ` Y ) ) )
9 5 8 syl 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> ( ( L ` A ) e. U <-> ( L ` A ) ( ||r ` Y ) ( 1r ` Y ) ) )
10 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
11 1 10 3 znzrhfo 
 |-  ( N e. NN0 -> L : ZZ -onto-> ( Base ` Y ) )
12 11 adantr 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> L : ZZ -onto-> ( Base ` Y ) )
13 fof 
 |-  ( L : ZZ -onto-> ( Base ` Y ) -> L : ZZ --> ( Base ` Y ) )
14 12 13 syl 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> L : ZZ --> ( Base ` Y ) )
15 ffvelrn 
 |-  ( ( L : ZZ --> ( Base ` Y ) /\ A e. ZZ ) -> ( L ` A ) e. ( Base ` Y ) )
16 14 15 sylancom 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> ( L ` A ) e. ( Base ` Y ) )
17 eqid 
 |-  ( .r ` Y ) = ( .r ` Y )
18 10 7 17 dvdsr2 
 |-  ( ( L ` A ) e. ( Base ` Y ) -> ( ( L ` A ) ( ||r ` Y ) ( 1r ` Y ) <-> E. x e. ( Base ` Y ) ( x ( .r ` Y ) ( L ` A ) ) = ( 1r ` Y ) ) )
19 16 18 syl 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> ( ( L ` A ) ( ||r ` Y ) ( 1r ` Y ) <-> E. x e. ( Base ` Y ) ( x ( .r ` Y ) ( L ` A ) ) = ( 1r ` Y ) ) )
20 forn 
 |-  ( L : ZZ -onto-> ( Base ` Y ) -> ran L = ( Base ` Y ) )
21 12 20 syl 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> ran L = ( Base ` Y ) )
22 21 rexeqdv 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> ( E. x e. ran L ( x ( .r ` Y ) ( L ` A ) ) = ( 1r ` Y ) <-> E. x e. ( Base ` Y ) ( x ( .r ` Y ) ( L ` A ) ) = ( 1r ` Y ) ) )
23 ffn 
 |-  ( L : ZZ --> ( Base ` Y ) -> L Fn ZZ )
24 oveq1 
 |-  ( x = ( L ` n ) -> ( x ( .r ` Y ) ( L ` A ) ) = ( ( L ` n ) ( .r ` Y ) ( L ` A ) ) )
25 24 eqeq1d 
 |-  ( x = ( L ` n ) -> ( ( x ( .r ` Y ) ( L ` A ) ) = ( 1r ` Y ) <-> ( ( L ` n ) ( .r ` Y ) ( L ` A ) ) = ( 1r ` Y ) ) )
26 25 rexrn 
 |-  ( L Fn ZZ -> ( E. x e. ran L ( x ( .r ` Y ) ( L ` A ) ) = ( 1r ` Y ) <-> E. n e. ZZ ( ( L ` n ) ( .r ` Y ) ( L ` A ) ) = ( 1r ` Y ) ) )
27 14 23 26 3syl 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> ( E. x e. ran L ( x ( .r ` Y ) ( L ` A ) ) = ( 1r ` Y ) <-> E. n e. ZZ ( ( L ` n ) ( .r ` Y ) ( L ` A ) ) = ( 1r ` Y ) ) )
28 22 27 bitr3d 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> ( E. x e. ( Base ` Y ) ( x ( .r ` Y ) ( L ` A ) ) = ( 1r ` Y ) <-> E. n e. ZZ ( ( L ` n ) ( .r ` Y ) ( L ` A ) ) = ( 1r ` Y ) ) )
29 crngring 
 |-  ( Y e. CRing -> Y e. Ring )
30 5 29 syl 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> Y e. Ring )
31 3 zrhrhm 
 |-  ( Y e. Ring -> L e. ( ZZring RingHom Y ) )
32 30 31 syl 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> L e. ( ZZring RingHom Y ) )
33 32 adantr 
 |-  ( ( ( N e. NN0 /\ A e. ZZ ) /\ n e. ZZ ) -> L e. ( ZZring RingHom Y ) )
34 simpr 
 |-  ( ( ( N e. NN0 /\ A e. ZZ ) /\ n e. ZZ ) -> n e. ZZ )
35 simplr 
 |-  ( ( ( N e. NN0 /\ A e. ZZ ) /\ n e. ZZ ) -> A e. ZZ )
36 zringbas 
 |-  ZZ = ( Base ` ZZring )
37 zringmulr 
 |-  x. = ( .r ` ZZring )
38 36 37 17 rhmmul 
 |-  ( ( L e. ( ZZring RingHom Y ) /\ n e. ZZ /\ A e. ZZ ) -> ( L ` ( n x. A ) ) = ( ( L ` n ) ( .r ` Y ) ( L ` A ) ) )
39 33 34 35 38 syl3anc 
 |-  ( ( ( N e. NN0 /\ A e. ZZ ) /\ n e. ZZ ) -> ( L ` ( n x. A ) ) = ( ( L ` n ) ( .r ` Y ) ( L ` A ) ) )
40 30 adantr 
 |-  ( ( ( N e. NN0 /\ A e. ZZ ) /\ n e. ZZ ) -> Y e. Ring )
41 3 6 zrh1 
 |-  ( Y e. Ring -> ( L ` 1 ) = ( 1r ` Y ) )
42 40 41 syl 
 |-  ( ( ( N e. NN0 /\ A e. ZZ ) /\ n e. ZZ ) -> ( L ` 1 ) = ( 1r ` Y ) )
43 39 42 eqeq12d 
 |-  ( ( ( N e. NN0 /\ A e. ZZ ) /\ n e. ZZ ) -> ( ( L ` ( n x. A ) ) = ( L ` 1 ) <-> ( ( L ` n ) ( .r ` Y ) ( L ` A ) ) = ( 1r ` Y ) ) )
44 simpll 
 |-  ( ( ( N e. NN0 /\ A e. ZZ ) /\ n e. ZZ ) -> N e. NN0 )
45 34 35 zmulcld 
 |-  ( ( ( N e. NN0 /\ A e. ZZ ) /\ n e. ZZ ) -> ( n x. A ) e. ZZ )
46 1zzd 
 |-  ( ( ( N e. NN0 /\ A e. ZZ ) /\ n e. ZZ ) -> 1 e. ZZ )
47 1 3 zndvds 
 |-  ( ( N e. NN0 /\ ( n x. A ) e. ZZ /\ 1 e. ZZ ) -> ( ( L ` ( n x. A ) ) = ( L ` 1 ) <-> N || ( ( n x. A ) - 1 ) ) )
48 44 45 46 47 syl3anc 
 |-  ( ( ( N e. NN0 /\ A e. ZZ ) /\ n e. ZZ ) -> ( ( L ` ( n x. A ) ) = ( L ` 1 ) <-> N || ( ( n x. A ) - 1 ) ) )
49 43 48 bitr3d 
 |-  ( ( ( N e. NN0 /\ A e. ZZ ) /\ n e. ZZ ) -> ( ( ( L ` n ) ( .r ` Y ) ( L ` A ) ) = ( 1r ` Y ) <-> N || ( ( n x. A ) - 1 ) ) )
50 49 rexbidva 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> ( E. n e. ZZ ( ( L ` n ) ( .r ` Y ) ( L ` A ) ) = ( 1r ` Y ) <-> E. n e. ZZ N || ( ( n x. A ) - 1 ) ) )
51 simplr 
 |-  ( ( ( N e. NN0 /\ A e. ZZ ) /\ ( n e. ZZ /\ N || ( ( n x. A ) - 1 ) ) ) -> A e. ZZ )
52 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
53 52 ad2antrr 
 |-  ( ( ( N e. NN0 /\ A e. ZZ ) /\ ( n e. ZZ /\ N || ( ( n x. A ) - 1 ) ) ) -> N e. ZZ )
54 gcddvds 
 |-  ( ( A e. ZZ /\ N e. ZZ ) -> ( ( A gcd N ) || A /\ ( A gcd N ) || N ) )
55 51 53 54 syl2anc 
 |-  ( ( ( N e. NN0 /\ A e. ZZ ) /\ ( n e. ZZ /\ N || ( ( n x. A ) - 1 ) ) ) -> ( ( A gcd N ) || A /\ ( A gcd N ) || N ) )
56 55 simpld 
 |-  ( ( ( N e. NN0 /\ A e. ZZ ) /\ ( n e. ZZ /\ N || ( ( n x. A ) - 1 ) ) ) -> ( A gcd N ) || A )
57 51 53 gcdcld 
 |-  ( ( ( N e. NN0 /\ A e. ZZ ) /\ ( n e. ZZ /\ N || ( ( n x. A ) - 1 ) ) ) -> ( A gcd N ) e. NN0 )
58 57 nn0zd 
 |-  ( ( ( N e. NN0 /\ A e. ZZ ) /\ ( n e. ZZ /\ N || ( ( n x. A ) - 1 ) ) ) -> ( A gcd N ) e. ZZ )
59 34 adantrr 
 |-  ( ( ( N e. NN0 /\ A e. ZZ ) /\ ( n e. ZZ /\ N || ( ( n x. A ) - 1 ) ) ) -> n e. ZZ )
60 dvdsmultr2 
 |-  ( ( ( A gcd N ) e. ZZ /\ n e. ZZ /\ A e. ZZ ) -> ( ( A gcd N ) || A -> ( A gcd N ) || ( n x. A ) ) )
61 58 59 51 60 syl3anc 
 |-  ( ( ( N e. NN0 /\ A e. ZZ ) /\ ( n e. ZZ /\ N || ( ( n x. A ) - 1 ) ) ) -> ( ( A gcd N ) || A -> ( A gcd N ) || ( n x. A ) ) )
62 56 61 mpd 
 |-  ( ( ( N e. NN0 /\ A e. ZZ ) /\ ( n e. ZZ /\ N || ( ( n x. A ) - 1 ) ) ) -> ( A gcd N ) || ( n x. A ) )
63 45 adantrr 
 |-  ( ( ( N e. NN0 /\ A e. ZZ ) /\ ( n e. ZZ /\ N || ( ( n x. A ) - 1 ) ) ) -> ( n x. A ) e. ZZ )
64 1zzd 
 |-  ( ( ( N e. NN0 /\ A e. ZZ ) /\ ( n e. ZZ /\ N || ( ( n x. A ) - 1 ) ) ) -> 1 e. ZZ )
65 peano2zm 
 |-  ( ( n x. A ) e. ZZ -> ( ( n x. A ) - 1 ) e. ZZ )
66 63 65 syl 
 |-  ( ( ( N e. NN0 /\ A e. ZZ ) /\ ( n e. ZZ /\ N || ( ( n x. A ) - 1 ) ) ) -> ( ( n x. A ) - 1 ) e. ZZ )
67 55 simprd 
 |-  ( ( ( N e. NN0 /\ A e. ZZ ) /\ ( n e. ZZ /\ N || ( ( n x. A ) - 1 ) ) ) -> ( A gcd N ) || N )
68 simprr 
 |-  ( ( ( N e. NN0 /\ A e. ZZ ) /\ ( n e. ZZ /\ N || ( ( n x. A ) - 1 ) ) ) -> N || ( ( n x. A ) - 1 ) )
69 58 53 66 67 68 dvdstrd 
 |-  ( ( ( N e. NN0 /\ A e. ZZ ) /\ ( n e. ZZ /\ N || ( ( n x. A ) - 1 ) ) ) -> ( A gcd N ) || ( ( n x. A ) - 1 ) )
70 dvdssub2 
 |-  ( ( ( ( A gcd N ) e. ZZ /\ ( n x. A ) e. ZZ /\ 1 e. ZZ ) /\ ( A gcd N ) || ( ( n x. A ) - 1 ) ) -> ( ( A gcd N ) || ( n x. A ) <-> ( A gcd N ) || 1 ) )
71 58 63 64 69 70 syl31anc 
 |-  ( ( ( N e. NN0 /\ A e. ZZ ) /\ ( n e. ZZ /\ N || ( ( n x. A ) - 1 ) ) ) -> ( ( A gcd N ) || ( n x. A ) <-> ( A gcd N ) || 1 ) )
72 62 71 mpbid 
 |-  ( ( ( N e. NN0 /\ A e. ZZ ) /\ ( n e. ZZ /\ N || ( ( n x. A ) - 1 ) ) ) -> ( A gcd N ) || 1 )
73 dvds1 
 |-  ( ( A gcd N ) e. NN0 -> ( ( A gcd N ) || 1 <-> ( A gcd N ) = 1 ) )
74 57 73 syl 
 |-  ( ( ( N e. NN0 /\ A e. ZZ ) /\ ( n e. ZZ /\ N || ( ( n x. A ) - 1 ) ) ) -> ( ( A gcd N ) || 1 <-> ( A gcd N ) = 1 ) )
75 72 74 mpbid 
 |-  ( ( ( N e. NN0 /\ A e. ZZ ) /\ ( n e. ZZ /\ N || ( ( n x. A ) - 1 ) ) ) -> ( A gcd N ) = 1 )
76 75 rexlimdvaa 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> ( E. n e. ZZ N || ( ( n x. A ) - 1 ) -> ( A gcd N ) = 1 ) )
77 simpr 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> A e. ZZ )
78 52 adantr 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> N e. ZZ )
79 bezout 
 |-  ( ( A e. ZZ /\ N e. ZZ ) -> E. n e. ZZ E. m e. ZZ ( A gcd N ) = ( ( A x. n ) + ( N x. m ) ) )
80 77 78 79 syl2anc 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> E. n e. ZZ E. m e. ZZ ( A gcd N ) = ( ( A x. n ) + ( N x. m ) ) )
81 eqeq1 
 |-  ( ( A gcd N ) = 1 -> ( ( A gcd N ) = ( ( A x. n ) + ( N x. m ) ) <-> 1 = ( ( A x. n ) + ( N x. m ) ) ) )
82 81 2rexbidv 
 |-  ( ( A gcd N ) = 1 -> ( E. n e. ZZ E. m e. ZZ ( A gcd N ) = ( ( A x. n ) + ( N x. m ) ) <-> E. n e. ZZ E. m e. ZZ 1 = ( ( A x. n ) + ( N x. m ) ) ) )
83 80 82 syl5ibcom 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> ( ( A gcd N ) = 1 -> E. n e. ZZ E. m e. ZZ 1 = ( ( A x. n ) + ( N x. m ) ) ) )
84 52 ad3antrrr 
 |-  ( ( ( ( N e. NN0 /\ A e. ZZ ) /\ n e. ZZ ) /\ m e. ZZ ) -> N e. ZZ )
85 dvdsmul1 
 |-  ( ( N e. ZZ /\ m e. ZZ ) -> N || ( N x. m ) )
86 84 85 sylancom 
 |-  ( ( ( ( N e. NN0 /\ A e. ZZ ) /\ n e. ZZ ) /\ m e. ZZ ) -> N || ( N x. m ) )
87 zmulcl 
 |-  ( ( N e. ZZ /\ m e. ZZ ) -> ( N x. m ) e. ZZ )
88 84 87 sylancom 
 |-  ( ( ( ( N e. NN0 /\ A e. ZZ ) /\ n e. ZZ ) /\ m e. ZZ ) -> ( N x. m ) e. ZZ )
89 dvdsnegb 
 |-  ( ( N e. ZZ /\ ( N x. m ) e. ZZ ) -> ( N || ( N x. m ) <-> N || -u ( N x. m ) ) )
90 84 88 89 syl2anc 
 |-  ( ( ( ( N e. NN0 /\ A e. ZZ ) /\ n e. ZZ ) /\ m e. ZZ ) -> ( N || ( N x. m ) <-> N || -u ( N x. m ) ) )
91 86 90 mpbid 
 |-  ( ( ( ( N e. NN0 /\ A e. ZZ ) /\ n e. ZZ ) /\ m e. ZZ ) -> N || -u ( N x. m ) )
92 35 adantr 
 |-  ( ( ( ( N e. NN0 /\ A e. ZZ ) /\ n e. ZZ ) /\ m e. ZZ ) -> A e. ZZ )
93 92 zcnd 
 |-  ( ( ( ( N e. NN0 /\ A e. ZZ ) /\ n e. ZZ ) /\ m e. ZZ ) -> A e. CC )
94 zcn 
 |-  ( n e. ZZ -> n e. CC )
95 94 ad2antlr 
 |-  ( ( ( ( N e. NN0 /\ A e. ZZ ) /\ n e. ZZ ) /\ m e. ZZ ) -> n e. CC )
96 93 95 mulcomd 
 |-  ( ( ( ( N e. NN0 /\ A e. ZZ ) /\ n e. ZZ ) /\ m e. ZZ ) -> ( A x. n ) = ( n x. A ) )
97 96 oveq1d 
 |-  ( ( ( ( N e. NN0 /\ A e. ZZ ) /\ n e. ZZ ) /\ m e. ZZ ) -> ( ( A x. n ) + ( N x. m ) ) = ( ( n x. A ) + ( N x. m ) ) )
98 95 93 mulcld 
 |-  ( ( ( ( N e. NN0 /\ A e. ZZ ) /\ n e. ZZ ) /\ m e. ZZ ) -> ( n x. A ) e. CC )
99 88 zcnd 
 |-  ( ( ( ( N e. NN0 /\ A e. ZZ ) /\ n e. ZZ ) /\ m e. ZZ ) -> ( N x. m ) e. CC )
100 98 99 subnegd 
 |-  ( ( ( ( N e. NN0 /\ A e. ZZ ) /\ n e. ZZ ) /\ m e. ZZ ) -> ( ( n x. A ) - -u ( N x. m ) ) = ( ( n x. A ) + ( N x. m ) ) )
101 97 100 eqtr4d 
 |-  ( ( ( ( N e. NN0 /\ A e. ZZ ) /\ n e. ZZ ) /\ m e. ZZ ) -> ( ( A x. n ) + ( N x. m ) ) = ( ( n x. A ) - -u ( N x. m ) ) )
102 101 oveq2d 
 |-  ( ( ( ( N e. NN0 /\ A e. ZZ ) /\ n e. ZZ ) /\ m e. ZZ ) -> ( ( n x. A ) - ( ( A x. n ) + ( N x. m ) ) ) = ( ( n x. A ) - ( ( n x. A ) - -u ( N x. m ) ) ) )
103 99 negcld 
 |-  ( ( ( ( N e. NN0 /\ A e. ZZ ) /\ n e. ZZ ) /\ m e. ZZ ) -> -u ( N x. m ) e. CC )
104 98 103 nncand 
 |-  ( ( ( ( N e. NN0 /\ A e. ZZ ) /\ n e. ZZ ) /\ m e. ZZ ) -> ( ( n x. A ) - ( ( n x. A ) - -u ( N x. m ) ) ) = -u ( N x. m ) )
105 102 104 eqtrd 
 |-  ( ( ( ( N e. NN0 /\ A e. ZZ ) /\ n e. ZZ ) /\ m e. ZZ ) -> ( ( n x. A ) - ( ( A x. n ) + ( N x. m ) ) ) = -u ( N x. m ) )
106 91 105 breqtrrd 
 |-  ( ( ( ( N e. NN0 /\ A e. ZZ ) /\ n e. ZZ ) /\ m e. ZZ ) -> N || ( ( n x. A ) - ( ( A x. n ) + ( N x. m ) ) ) )
107 oveq2 
 |-  ( 1 = ( ( A x. n ) + ( N x. m ) ) -> ( ( n x. A ) - 1 ) = ( ( n x. A ) - ( ( A x. n ) + ( N x. m ) ) ) )
108 107 breq2d 
 |-  ( 1 = ( ( A x. n ) + ( N x. m ) ) -> ( N || ( ( n x. A ) - 1 ) <-> N || ( ( n x. A ) - ( ( A x. n ) + ( N x. m ) ) ) ) )
109 106 108 syl5ibrcom 
 |-  ( ( ( ( N e. NN0 /\ A e. ZZ ) /\ n e. ZZ ) /\ m e. ZZ ) -> ( 1 = ( ( A x. n ) + ( N x. m ) ) -> N || ( ( n x. A ) - 1 ) ) )
110 109 rexlimdva 
 |-  ( ( ( N e. NN0 /\ A e. ZZ ) /\ n e. ZZ ) -> ( E. m e. ZZ 1 = ( ( A x. n ) + ( N x. m ) ) -> N || ( ( n x. A ) - 1 ) ) )
111 110 reximdva 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> ( E. n e. ZZ E. m e. ZZ 1 = ( ( A x. n ) + ( N x. m ) ) -> E. n e. ZZ N || ( ( n x. A ) - 1 ) ) )
112 83 111 syld 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> ( ( A gcd N ) = 1 -> E. n e. ZZ N || ( ( n x. A ) - 1 ) ) )
113 76 112 impbid 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> ( E. n e. ZZ N || ( ( n x. A ) - 1 ) <-> ( A gcd N ) = 1 ) )
114 28 50 113 3bitrd 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> ( E. x e. ( Base ` Y ) ( x ( .r ` Y ) ( L ` A ) ) = ( 1r ` Y ) <-> ( A gcd N ) = 1 ) )
115 9 19 114 3bitrd 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> ( ( L ` A ) e. U <-> ( A gcd N ) = 1 ) )