Metamath Proof Explorer

Theorem znidomb

Description: The Z/nZ structure is a domain (and hence a field) precisely when n is prime. (Contributed by Mario Carneiro, 15-Jun-2015)

Ref Expression
Hypothesis zntos.y 
|- Y = ( Z/nZ ` N )
Assertion znidomb 
|- ( N e. NN -> ( Y e. IDomn <-> N e. Prime ) )

Proof

Step Hyp Ref Expression
1 zntos.y 
 |-  Y = ( Z/nZ ` N )
2 2z 
 |-  2 e. ZZ
3 2 a1i 
 |-  ( ( N e. NN /\ Y e. IDomn ) -> 2 e. ZZ )
4 nnz 
 |-  ( N e. NN -> N e. ZZ )
5 4 adantr 
 |-  ( ( N e. NN /\ Y e. IDomn ) -> N e. ZZ )
6 hash2 
 |-  ( # ` 2o ) = 2
7 isidom 
 |-  ( Y e. IDomn <-> ( Y e. CRing /\ Y e. Domn ) )
8 7 simprbi 
 |-  ( Y e. IDomn -> Y e. Domn )
9 domnnzr 
 |-  ( Y e. Domn -> Y e. NzRing )
10 8 9 syl 
 |-  ( Y e. IDomn -> Y e. NzRing )
11 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
12 11 isnzr2 
 |-  ( Y e. NzRing <-> ( Y e. Ring /\ 2o ~<_ ( Base ` Y ) ) )
13 12 simprbi 
 |-  ( Y e. NzRing -> 2o ~<_ ( Base ` Y ) )
14 10 13 syl 
 |-  ( Y e. IDomn -> 2o ~<_ ( Base ` Y ) )
15 14 adantl 
 |-  ( ( N e. NN /\ Y e. IDomn ) -> 2o ~<_ ( Base ` Y ) )
16 df2o2 
 |-  2o = { (/) , { (/) } }
17 prfi 
 |-  { (/) , { (/) } } e. Fin
18 16 17 eqeltri 
 |-  2o e. Fin
19 fvex 
 |-  ( Base ` Y ) e. _V
20 hashdom 
 |-  ( ( 2o e. Fin /\ ( Base ` Y ) e. _V ) -> ( ( # ` 2o ) <_ ( # ` ( Base ` Y ) ) <-> 2o ~<_ ( Base ` Y ) ) )
21 18 19 20 mp2an 
 |-  ( ( # ` 2o ) <_ ( # ` ( Base ` Y ) ) <-> 2o ~<_ ( Base ` Y ) )
22 15 21 sylibr 
 |-  ( ( N e. NN /\ Y e. IDomn ) -> ( # ` 2o ) <_ ( # ` ( Base ` Y ) ) )
23 6 22 eqbrtrrid 
 |-  ( ( N e. NN /\ Y e. IDomn ) -> 2 <_ ( # ` ( Base ` Y ) ) )
24 1 11 znhash 
 |-  ( N e. NN -> ( # ` ( Base ` Y ) ) = N )
25 24 adantr 
 |-  ( ( N e. NN /\ Y e. IDomn ) -> ( # ` ( Base ` Y ) ) = N )
26 23 25 breqtrd 
 |-  ( ( N e. NN /\ Y e. IDomn ) -> 2 <_ N )
27 eluz2 
 |-  ( N e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ N e. ZZ /\ 2 <_ N ) )
28 3 5 26 27 syl3anbrc 
 |-  ( ( N e. NN /\ Y e. IDomn ) -> N e. ( ZZ>= ` 2 ) )
29 nncn 
 |-  ( N e. NN -> N e. CC )
30 29 ad2antrr 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> N e. CC )
31 nncn 
 |-  ( x e. NN -> x e. CC )
32 31 ad2antrl 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> x e. CC )
33 nnne0 
 |-  ( x e. NN -> x =/= 0 )
34 33 ad2antrl 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> x =/= 0 )
35 30 32 34 divcan1d 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> ( ( N / x ) x. x ) = N )
36 35 fveq2d 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> ( ( ZRHom ` Y ) ` ( ( N / x ) x. x ) ) = ( ( ZRHom ` Y ) ` N ) )
37 8 ad2antlr 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> Y e. Domn )
38 domnring 
 |-  ( Y e. Domn -> Y e. Ring )
39 37 38 syl 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> Y e. Ring )
40 eqid 
 |-  ( ZRHom ` Y ) = ( ZRHom ` Y )
41 40 zrhrhm 
 |-  ( Y e. Ring -> ( ZRHom ` Y ) e. ( ZZring RingHom Y ) )
42 39 41 syl 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> ( ZRHom ` Y ) e. ( ZZring RingHom Y ) )
43 simprr 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> x || N )
44 nnz 
 |-  ( x e. NN -> x e. ZZ )
45 44 ad2antrl 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> x e. ZZ )
46 4 ad2antrr 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> N e. ZZ )
47 dvdsval2 
 |-  ( ( x e. ZZ /\ x =/= 0 /\ N e. ZZ ) -> ( x || N <-> ( N / x ) e. ZZ ) )
48 45 34 46 47 syl3anc 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> ( x || N <-> ( N / x ) e. ZZ ) )
49 43 48 mpbid 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> ( N / x ) e. ZZ )
50 zringbas 
 |-  ZZ = ( Base ` ZZring )
51 zringmulr 
 |-  x. = ( .r ` ZZring )
52 eqid 
 |-  ( .r ` Y ) = ( .r ` Y )
53 50 51 52 rhmmul 
 |-  ( ( ( ZRHom ` Y ) e. ( ZZring RingHom Y ) /\ ( N / x ) e. ZZ /\ x e. ZZ ) -> ( ( ZRHom ` Y ) ` ( ( N / x ) x. x ) ) = ( ( ( ZRHom ` Y ) ` ( N / x ) ) ( .r ` Y ) ( ( ZRHom ` Y ) ` x ) ) )
54 42 49 45 53 syl3anc 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> ( ( ZRHom ` Y ) ` ( ( N / x ) x. x ) ) = ( ( ( ZRHom ` Y ) ` ( N / x ) ) ( .r ` Y ) ( ( ZRHom ` Y ) ` x ) ) )
55 iddvds 
 |-  ( N e. ZZ -> N || N )
56 46 55 syl 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> N || N )
57 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
58 57 ad2antrr 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> N e. NN0 )
59 eqid 
 |-  ( 0g ` Y ) = ( 0g ` Y )
60 1 40 59 zndvds0 
 |-  ( ( N e. NN0 /\ N e. ZZ ) -> ( ( ( ZRHom ` Y ) ` N ) = ( 0g ` Y ) <-> N || N ) )
61 58 46 60 syl2anc 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> ( ( ( ZRHom ` Y ) ` N ) = ( 0g ` Y ) <-> N || N ) )
62 56 61 mpbird 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> ( ( ZRHom ` Y ) ` N ) = ( 0g ` Y ) )
63 36 54 62 3eqtr3d 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> ( ( ( ZRHom ` Y ) ` ( N / x ) ) ( .r ` Y ) ( ( ZRHom ` Y ) ` x ) ) = ( 0g ` Y ) )
64 50 11 rhmf 
 |-  ( ( ZRHom ` Y ) e. ( ZZring RingHom Y ) -> ( ZRHom ` Y ) : ZZ --> ( Base ` Y ) )
65 42 64 syl 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> ( ZRHom ` Y ) : ZZ --> ( Base ` Y ) )
66 65 49 ffvelrnd 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> ( ( ZRHom ` Y ) ` ( N / x ) ) e. ( Base ` Y ) )
67 65 45 ffvelrnd 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> ( ( ZRHom ` Y ) ` x ) e. ( Base ` Y ) )
68 11 52 59 domneq0 
 |-  ( ( Y e. Domn /\ ( ( ZRHom ` Y ) ` ( N / x ) ) e. ( Base ` Y ) /\ ( ( ZRHom ` Y ) ` x ) e. ( Base ` Y ) ) -> ( ( ( ( ZRHom ` Y ) ` ( N / x ) ) ( .r ` Y ) ( ( ZRHom ` Y ) ` x ) ) = ( 0g ` Y ) <-> ( ( ( ZRHom ` Y ) ` ( N / x ) ) = ( 0g ` Y ) \/ ( ( ZRHom ` Y ) ` x ) = ( 0g ` Y ) ) ) )
69 37 66 67 68 syl3anc 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> ( ( ( ( ZRHom ` Y ) ` ( N / x ) ) ( .r ` Y ) ( ( ZRHom ` Y ) ` x ) ) = ( 0g ` Y ) <-> ( ( ( ZRHom ` Y ) ` ( N / x ) ) = ( 0g ` Y ) \/ ( ( ZRHom ` Y ) ` x ) = ( 0g ` Y ) ) ) )
70 63 69 mpbid 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> ( ( ( ZRHom ` Y ) ` ( N / x ) ) = ( 0g ` Y ) \/ ( ( ZRHom ` Y ) ` x ) = ( 0g ` Y ) ) )
71 1 40 59 zndvds0 
 |-  ( ( N e. NN0 /\ ( N / x ) e. ZZ ) -> ( ( ( ZRHom ` Y ) ` ( N / x ) ) = ( 0g ` Y ) <-> N || ( N / x ) ) )
72 58 49 71 syl2anc 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> ( ( ( ZRHom ` Y ) ` ( N / x ) ) = ( 0g ` Y ) <-> N || ( N / x ) ) )
73 nnre 
 |-  ( N e. NN -> N e. RR )
74 73 ad2antrr 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> N e. RR )
75 nnre 
 |-  ( x e. NN -> x e. RR )
76 75 ad2antrl 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> x e. RR )
77 nngt0 
 |-  ( N e. NN -> 0 < N )
78 77 ad2antrr 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> 0 < N )
79 nngt0 
 |-  ( x e. NN -> 0 < x )
80 79 ad2antrl 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> 0 < x )
81 74 76 78 80 divgt0d 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> 0 < ( N / x ) )
82 elnnz 
 |-  ( ( N / x ) e. NN <-> ( ( N / x ) e. ZZ /\ 0 < ( N / x ) ) )
83 49 81 82 sylanbrc 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> ( N / x ) e. NN )
84 dvdsle 
 |-  ( ( N e. ZZ /\ ( N / x ) e. NN ) -> ( N || ( N / x ) -> N <_ ( N / x ) ) )
85 46 83 84 syl2anc 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> ( N || ( N / x ) -> N <_ ( N / x ) ) )
86 1red 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> 1 e. RR )
87 0lt1 
 |-  0 < 1
88 87 a1i 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> 0 < 1 )
89 lediv2 
 |-  ( ( ( x e. RR /\ 0 < x ) /\ ( 1 e. RR /\ 0 < 1 ) /\ ( N e. RR /\ 0 < N ) ) -> ( x <_ 1 <-> ( N / 1 ) <_ ( N / x ) ) )
90 76 80 86 88 74 78 89 syl222anc 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> ( x <_ 1 <-> ( N / 1 ) <_ ( N / x ) ) )
91 nnle1eq1 
 |-  ( x e. NN -> ( x <_ 1 <-> x = 1 ) )
92 91 ad2antrl 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> ( x <_ 1 <-> x = 1 ) )
93 30 div1d 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> ( N / 1 ) = N )
94 93 breq1d 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> ( ( N / 1 ) <_ ( N / x ) <-> N <_ ( N / x ) ) )
95 90 92 94 3bitr3rd 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> ( N <_ ( N / x ) <-> x = 1 ) )
96 85 95 sylibd 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> ( N || ( N / x ) -> x = 1 ) )
97 72 96 sylbid 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> ( ( ( ZRHom ` Y ) ` ( N / x ) ) = ( 0g ` Y ) -> x = 1 ) )
98 1 40 59 zndvds0 
 |-  ( ( N e. NN0 /\ x e. ZZ ) -> ( ( ( ZRHom ` Y ) ` x ) = ( 0g ` Y ) <-> N || x ) )
99 58 45 98 syl2anc 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> ( ( ( ZRHom ` Y ) ` x ) = ( 0g ` Y ) <-> N || x ) )
100 nnnn0 
 |-  ( x e. NN -> x e. NN0 )
101 100 ad2antrl 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> x e. NN0 )
102 dvdseq 
 |-  ( ( ( x e. NN0 /\ N e. NN0 ) /\ ( x || N /\ N || x ) ) -> x = N )
103 102 expr 
 |-  ( ( ( x e. NN0 /\ N e. NN0 ) /\ x || N ) -> ( N || x -> x = N ) )
104 101 58 43 103 syl21anc 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> ( N || x -> x = N ) )
105 99 104 sylbid 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> ( ( ( ZRHom ` Y ) ` x ) = ( 0g ` Y ) -> x = N ) )
106 97 105 orim12d 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> ( ( ( ( ZRHom ` Y ) ` ( N / x ) ) = ( 0g ` Y ) \/ ( ( ZRHom ` Y ) ` x ) = ( 0g ` Y ) ) -> ( x = 1 \/ x = N ) ) )
107 70 106 mpd 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ ( x e. NN /\ x || N ) ) -> ( x = 1 \/ x = N ) )
108 107 expr 
 |-  ( ( ( N e. NN /\ Y e. IDomn ) /\ x e. NN ) -> ( x || N -> ( x = 1 \/ x = N ) ) )
109 108 ralrimiva 
 |-  ( ( N e. NN /\ Y e. IDomn ) -> A. x e. NN ( x || N -> ( x = 1 \/ x = N ) ) )
110 isprm2 
 |-  ( N e. Prime <-> ( N e. ( ZZ>= ` 2 ) /\ A. x e. NN ( x || N -> ( x = 1 \/ x = N ) ) ) )
111 28 109 110 sylanbrc 
 |-  ( ( N e. NN /\ Y e. IDomn ) -> N e. Prime )
112 111 ex 
 |-  ( N e. NN -> ( Y e. IDomn -> N e. Prime ) )
113 1 znfld 
 |-  ( N e. Prime -> Y e. Field )
114 fldidom 
 |-  ( Y e. Field -> Y e. IDomn )
115 113 114 syl 
 |-  ( N e. Prime -> Y e. IDomn )
116 112 115 impbid1 
 |-  ( N e. NN -> ( Y e. IDomn <-> N e. Prime ) )