Metamath Proof Explorer

Theorem znfld

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

Ref Expression
Hypothesis zntos.y 
|- Y = ( Z/nZ ` N )
Assertion znfld 
|- ( N e. Prime -> Y e. Field )

Proof

Step Hyp Ref Expression
1 zntos.y 
 |-  Y = ( Z/nZ ` N )
2 prmnn 
 |-  ( N e. Prime -> N e. NN )
3 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
4 2 3 syl 
 |-  ( N e. Prime -> N e. NN0 )
5 1 zncrng 
 |-  ( N e. NN0 -> Y e. CRing )
6 4 5 syl 
 |-  ( N e. Prime -> Y e. CRing )
7 crngring 
 |-  ( Y e. CRing -> Y e. Ring )
8 2 3 5 7 4syl 
 |-  ( N e. Prime -> Y e. Ring )
9 hash2 
 |-  ( # ` 2o ) = 2
10 prmuz2 
 |-  ( N e. Prime -> N e. ( ZZ>= ` 2 ) )
11 eluzle 
 |-  ( N e. ( ZZ>= ` 2 ) -> 2 <_ N )
12 10 11 syl 
 |-  ( N e. Prime -> 2 <_ N )
13 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
14 1 13 znhash 
 |-  ( N e. NN -> ( # ` ( Base ` Y ) ) = N )
15 2 14 syl 
 |-  ( N e. Prime -> ( # ` ( Base ` Y ) ) = N )
16 12 15 breqtrrd 
 |-  ( N e. Prime -> 2 <_ ( # ` ( Base ` Y ) ) )
17 9 16 eqbrtrid 
 |-  ( N e. Prime -> ( # ` 2o ) <_ ( # ` ( Base ` Y ) ) )
18 2onn 
 |-  2o e. _om
19 nnfi 
 |-  ( 2o e. _om -> 2o e. Fin )
20 18 19 ax-mp 
 |-  2o e. Fin
21 fvex 
 |-  ( Base ` Y ) e. _V
22 hashdom 
 |-  ( ( 2o e. Fin /\ ( Base ` Y ) e. _V ) -> ( ( # ` 2o ) <_ ( # ` ( Base ` Y ) ) <-> 2o ~<_ ( Base ` Y ) ) )
23 20 21 22 mp2an 
 |-  ( ( # ` 2o ) <_ ( # ` ( Base ` Y ) ) <-> 2o ~<_ ( Base ` Y ) )
24 17 23 sylib 
 |-  ( N e. Prime -> 2o ~<_ ( Base ` Y ) )
25 13 isnzr2 
 |-  ( Y e. NzRing <-> ( Y e. Ring /\ 2o ~<_ ( Base ` Y ) ) )
26 8 24 25 sylanbrc 
 |-  ( N e. Prime -> Y e. NzRing )
27 eqid 
 |-  ( ZRHom ` Y ) = ( ZRHom ` Y )
28 1 13 27 znzrhfo 
 |-  ( N e. NN0 -> ( ZRHom ` Y ) : ZZ -onto-> ( Base ` Y ) )
29 4 28 syl 
 |-  ( N e. Prime -> ( ZRHom ` Y ) : ZZ -onto-> ( Base ` Y ) )
30 foelrn 
 |-  ( ( ( ZRHom ` Y ) : ZZ -onto-> ( Base ` Y ) /\ x e. ( Base ` Y ) ) -> E. z e. ZZ x = ( ( ZRHom ` Y ) ` z ) )
31 foelrn 
 |-  ( ( ( ZRHom ` Y ) : ZZ -onto-> ( Base ` Y ) /\ y e. ( Base ` Y ) ) -> E. w e. ZZ y = ( ( ZRHom ` Y ) ` w ) )
32 30 31 anim12dan 
 |-  ( ( ( ZRHom ` Y ) : ZZ -onto-> ( Base ` Y ) /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) ) ) -> ( E. z e. ZZ x = ( ( ZRHom ` Y ) ` z ) /\ E. w e. ZZ y = ( ( ZRHom ` Y ) ` w ) ) )
33 29 32 sylan 
 |-  ( ( N e. Prime /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) ) ) -> ( E. z e. ZZ x = ( ( ZRHom ` Y ) ` z ) /\ E. w e. ZZ y = ( ( ZRHom ` Y ) ` w ) ) )
34 reeanv 
 |-  ( E. z e. ZZ E. w e. ZZ ( x = ( ( ZRHom ` Y ) ` z ) /\ y = ( ( ZRHom ` Y ) ` w ) ) <-> ( E. z e. ZZ x = ( ( ZRHom ` Y ) ` z ) /\ E. w e. ZZ y = ( ( ZRHom ` Y ) ` w ) ) )
35 euclemma 
 |-  ( ( N e. Prime /\ z e. ZZ /\ w e. ZZ ) -> ( N || ( z x. w ) <-> ( N || z \/ N || w ) ) )
36 35 3expb 
 |-  ( ( N e. Prime /\ ( z e. ZZ /\ w e. ZZ ) ) -> ( N || ( z x. w ) <-> ( N || z \/ N || w ) ) )
37 8 adantr 
 |-  ( ( N e. Prime /\ ( z e. ZZ /\ w e. ZZ ) ) -> Y e. Ring )
38 27 zrhrhm 
 |-  ( Y e. Ring -> ( ZRHom ` Y ) e. ( ZZring RingHom Y ) )
39 37 38 syl 
 |-  ( ( N e. Prime /\ ( z e. ZZ /\ w e. ZZ ) ) -> ( ZRHom ` Y ) e. ( ZZring RingHom Y ) )
40 simprl 
 |-  ( ( N e. Prime /\ ( z e. ZZ /\ w e. ZZ ) ) -> z e. ZZ )
41 simprr 
 |-  ( ( N e. Prime /\ ( z e. ZZ /\ w e. ZZ ) ) -> w e. ZZ )
42 zringbas 
 |-  ZZ = ( Base ` ZZring )
43 zringmulr 
 |-  x. = ( .r ` ZZring )
44 eqid 
 |-  ( .r ` Y ) = ( .r ` Y )
45 42 43 44 rhmmul 
 |-  ( ( ( ZRHom ` Y ) e. ( ZZring RingHom Y ) /\ z e. ZZ /\ w e. ZZ ) -> ( ( ZRHom ` Y ) ` ( z x. w ) ) = ( ( ( ZRHom ` Y ) ` z ) ( .r ` Y ) ( ( ZRHom ` Y ) ` w ) ) )
46 39 40 41 45 syl3anc 
 |-  ( ( N e. Prime /\ ( z e. ZZ /\ w e. ZZ ) ) -> ( ( ZRHom ` Y ) ` ( z x. w ) ) = ( ( ( ZRHom ` Y ) ` z ) ( .r ` Y ) ( ( ZRHom ` Y ) ` w ) ) )
47 46 eqeq1d 
 |-  ( ( N e. Prime /\ ( z e. ZZ /\ w e. ZZ ) ) -> ( ( ( ZRHom ` Y ) ` ( z x. w ) ) = ( 0g ` Y ) <-> ( ( ( ZRHom ` Y ) ` z ) ( .r ` Y ) ( ( ZRHom ` Y ) ` w ) ) = ( 0g ` Y ) ) )
48 zmulcl 
 |-  ( ( z e. ZZ /\ w e. ZZ ) -> ( z x. w ) e. ZZ )
49 eqid 
 |-  ( 0g ` Y ) = ( 0g ` Y )
50 1 27 49 zndvds0 
 |-  ( ( N e. NN0 /\ ( z x. w ) e. ZZ ) -> ( ( ( ZRHom ` Y ) ` ( z x. w ) ) = ( 0g ` Y ) <-> N || ( z x. w ) ) )
51 4 48 50 syl2an 
 |-  ( ( N e. Prime /\ ( z e. ZZ /\ w e. ZZ ) ) -> ( ( ( ZRHom ` Y ) ` ( z x. w ) ) = ( 0g ` Y ) <-> N || ( z x. w ) ) )
52 47 51 bitr3d 
 |-  ( ( N e. Prime /\ ( z e. ZZ /\ w e. ZZ ) ) -> ( ( ( ( ZRHom ` Y ) ` z ) ( .r ` Y ) ( ( ZRHom ` Y ) ` w ) ) = ( 0g ` Y ) <-> N || ( z x. w ) ) )
53 1 27 49 zndvds0 
 |-  ( ( N e. NN0 /\ z e. ZZ ) -> ( ( ( ZRHom ` Y ) ` z ) = ( 0g ` Y ) <-> N || z ) )
54 4 40 53 syl2an2r 
 |-  ( ( N e. Prime /\ ( z e. ZZ /\ w e. ZZ ) ) -> ( ( ( ZRHom ` Y ) ` z ) = ( 0g ` Y ) <-> N || z ) )
55 1 27 49 zndvds0 
 |-  ( ( N e. NN0 /\ w e. ZZ ) -> ( ( ( ZRHom ` Y ) ` w ) = ( 0g ` Y ) <-> N || w ) )
56 4 41 55 syl2an2r 
 |-  ( ( N e. Prime /\ ( z e. ZZ /\ w e. ZZ ) ) -> ( ( ( ZRHom ` Y ) ` w ) = ( 0g ` Y ) <-> N || w ) )
57 54 56 orbi12d 
 |-  ( ( N e. Prime /\ ( z e. ZZ /\ w e. ZZ ) ) -> ( ( ( ( ZRHom ` Y ) ` z ) = ( 0g ` Y ) \/ ( ( ZRHom ` Y ) ` w ) = ( 0g ` Y ) ) <-> ( N || z \/ N || w ) ) )
58 36 52 57 3bitr4d 
 |-  ( ( N e. Prime /\ ( z e. ZZ /\ w e. ZZ ) ) -> ( ( ( ( ZRHom ` Y ) ` z ) ( .r ` Y ) ( ( ZRHom ` Y ) ` w ) ) = ( 0g ` Y ) <-> ( ( ( ZRHom ` Y ) ` z ) = ( 0g ` Y ) \/ ( ( ZRHom ` Y ) ` w ) = ( 0g ` Y ) ) ) )
59 58 biimpd 
 |-  ( ( N e. Prime /\ ( z e. ZZ /\ w e. ZZ ) ) -> ( ( ( ( ZRHom ` Y ) ` z ) ( .r ` Y ) ( ( ZRHom ` Y ) ` w ) ) = ( 0g ` Y ) -> ( ( ( ZRHom ` Y ) ` z ) = ( 0g ` Y ) \/ ( ( ZRHom ` Y ) ` w ) = ( 0g ` Y ) ) ) )
60 oveq12 
 |-  ( ( x = ( ( ZRHom ` Y ) ` z ) /\ y = ( ( ZRHom ` Y ) ` w ) ) -> ( x ( .r ` Y ) y ) = ( ( ( ZRHom ` Y ) ` z ) ( .r ` Y ) ( ( ZRHom ` Y ) ` w ) ) )
61 60 eqeq1d 
 |-  ( ( x = ( ( ZRHom ` Y ) ` z ) /\ y = ( ( ZRHom ` Y ) ` w ) ) -> ( ( x ( .r ` Y ) y ) = ( 0g ` Y ) <-> ( ( ( ZRHom ` Y ) ` z ) ( .r ` Y ) ( ( ZRHom ` Y ) ` w ) ) = ( 0g ` Y ) ) )
62 eqeq1 
 |-  ( x = ( ( ZRHom ` Y ) ` z ) -> ( x = ( 0g ` Y ) <-> ( ( ZRHom ` Y ) ` z ) = ( 0g ` Y ) ) )
63 62 orbi1d 
 |-  ( x = ( ( ZRHom ` Y ) ` z ) -> ( ( x = ( 0g ` Y ) \/ y = ( 0g ` Y ) ) <-> ( ( ( ZRHom ` Y ) ` z ) = ( 0g ` Y ) \/ y = ( 0g ` Y ) ) ) )
64 eqeq1 
 |-  ( y = ( ( ZRHom ` Y ) ` w ) -> ( y = ( 0g ` Y ) <-> ( ( ZRHom ` Y ) ` w ) = ( 0g ` Y ) ) )
65 64 orbi2d 
 |-  ( y = ( ( ZRHom ` Y ) ` w ) -> ( ( ( ( ZRHom ` Y ) ` z ) = ( 0g ` Y ) \/ y = ( 0g ` Y ) ) <-> ( ( ( ZRHom ` Y ) ` z ) = ( 0g ` Y ) \/ ( ( ZRHom ` Y ) ` w ) = ( 0g ` Y ) ) ) )
66 63 65 sylan9bb 
 |-  ( ( x = ( ( ZRHom ` Y ) ` z ) /\ y = ( ( ZRHom ` Y ) ` w ) ) -> ( ( x = ( 0g ` Y ) \/ y = ( 0g ` Y ) ) <-> ( ( ( ZRHom ` Y ) ` z ) = ( 0g ` Y ) \/ ( ( ZRHom ` Y ) ` w ) = ( 0g ` Y ) ) ) )
67 61 66 imbi12d 
 |-  ( ( x = ( ( ZRHom ` Y ) ` z ) /\ y = ( ( ZRHom ` Y ) ` w ) ) -> ( ( ( x ( .r ` Y ) y ) = ( 0g ` Y ) -> ( x = ( 0g ` Y ) \/ y = ( 0g ` Y ) ) ) <-> ( ( ( ( ZRHom ` Y ) ` z ) ( .r ` Y ) ( ( ZRHom ` Y ) ` w ) ) = ( 0g ` Y ) -> ( ( ( ZRHom ` Y ) ` z ) = ( 0g ` Y ) \/ ( ( ZRHom ` Y ) ` w ) = ( 0g ` Y ) ) ) ) )
68 59 67 syl5ibrcom 
 |-  ( ( N e. Prime /\ ( z e. ZZ /\ w e. ZZ ) ) -> ( ( x = ( ( ZRHom ` Y ) ` z ) /\ y = ( ( ZRHom ` Y ) ` w ) ) -> ( ( x ( .r ` Y ) y ) = ( 0g ` Y ) -> ( x = ( 0g ` Y ) \/ y = ( 0g ` Y ) ) ) ) )
69 68 rexlimdvva 
 |-  ( N e. Prime -> ( E. z e. ZZ E. w e. ZZ ( x = ( ( ZRHom ` Y ) ` z ) /\ y = ( ( ZRHom ` Y ) ` w ) ) -> ( ( x ( .r ` Y ) y ) = ( 0g ` Y ) -> ( x = ( 0g ` Y ) \/ y = ( 0g ` Y ) ) ) ) )
70 34 69 syl5bir 
 |-  ( N e. Prime -> ( ( E. z e. ZZ x = ( ( ZRHom ` Y ) ` z ) /\ E. w e. ZZ y = ( ( ZRHom ` Y ) ` w ) ) -> ( ( x ( .r ` Y ) y ) = ( 0g ` Y ) -> ( x = ( 0g ` Y ) \/ y = ( 0g ` Y ) ) ) ) )
71 70 imp 
 |-  ( ( N e. Prime /\ ( E. z e. ZZ x = ( ( ZRHom ` Y ) ` z ) /\ E. w e. ZZ y = ( ( ZRHom ` Y ) ` w ) ) ) -> ( ( x ( .r ` Y ) y ) = ( 0g ` Y ) -> ( x = ( 0g ` Y ) \/ y = ( 0g ` Y ) ) ) )
72 33 71 syldan 
 |-  ( ( N e. Prime /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) ) ) -> ( ( x ( .r ` Y ) y ) = ( 0g ` Y ) -> ( x = ( 0g ` Y ) \/ y = ( 0g ` Y ) ) ) )
73 72 ralrimivva 
 |-  ( N e. Prime -> A. x e. ( Base ` Y ) A. y e. ( Base ` Y ) ( ( x ( .r ` Y ) y ) = ( 0g ` Y ) -> ( x = ( 0g ` Y ) \/ y = ( 0g ` Y ) ) ) )
74 13 44 49 isdomn 
 |-  ( Y e. Domn <-> ( Y e. NzRing /\ A. x e. ( Base ` Y ) A. y e. ( Base ` Y ) ( ( x ( .r ` Y ) y ) = ( 0g ` Y ) -> ( x = ( 0g ` Y ) \/ y = ( 0g ` Y ) ) ) ) )
75 26 73 74 sylanbrc 
 |-  ( N e. Prime -> Y e. Domn )
76 isidom 
 |-  ( Y e. IDomn <-> ( Y e. CRing /\ Y e. Domn ) )
77 6 75 76 sylanbrc 
 |-  ( N e. Prime -> Y e. IDomn )
78 1 13 znfi 
 |-  ( N e. NN -> ( Base ` Y ) e. Fin )
79 2 78 syl 
 |-  ( N e. Prime -> ( Base ` Y ) e. Fin )
80 13 fiidomfld 
 |-  ( ( Base ` Y ) e. Fin -> ( Y e. IDomn <-> Y e. Field ) )
81 79 80 syl 
 |-  ( N e. Prime -> ( Y e. IDomn <-> Y e. Field ) )
82 77 81 mpbid 
 |-  ( N e. Prime -> Y e. Field )