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 = ℤ / N ℤ$
	Assertion	znfld	$⊢ N \in ℙ \to Y \in Field$

Proof

Step	Hyp	Ref	Expression
1		zntos.y	$⊢ Y = ℤ / N ℤ$
2		prmnn	$⊢ N \in ℙ \to N \in ℕ$
3		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
4	2 3	syl	$⊢ N \in ℙ \to N \in ℕ_{0}$
5	1	zncrng	$⊢ N \in ℕ_{0} \to Y \in CRing$
6	4 5	syl	$⊢ N \in ℙ \to Y \in CRing$
7		crngring	$⊢ Y \in CRing \to Y \in Ring$
8	2 3 5 7	4syl	$⊢ N \in ℙ \to Y \in Ring$
9		hash2	$⊢ \|2_{𝑜}\| = 2$
10		prmuz2	$⊢ N \in ℙ \to N \in ℤ_{\geq 2}$
11		eluzle	$⊢ N \in ℤ_{\geq 2} \to 2 \leq N$
12	10 11	syl	$⊢ N \in ℙ \to 2 \leq N$
13		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
14	1 13	znhash	$⊢ N \in ℕ \to \|{Base}_{Y}\| = N$
15	2 14	syl	$⊢ N \in ℙ \to \|{Base}_{Y}\| = N$
16	12 15	breqtrrd	$⊢ N \in ℙ \to 2 \leq \|{Base}_{Y}\|$
17	9 16	eqbrtrid	$⊢ N \in ℙ \to \|2_{𝑜}\| \leq \|{Base}_{Y}\|$
18		2onn	$⊢ 2_{𝑜} \in ω$
19		nnfi	$⊢ 2_{𝑜} \in ω \to 2_{𝑜} \in Fin$
20	18 19	ax-mp	$⊢ 2_{𝑜} \in Fin$
21		fvex	$⊢ {Base}_{Y} \in V$
22		hashdom	$⊢ (2_{𝑜} \in Fin \land {Base}_{Y} \in V) \to (\|2_{𝑜}\| \leq \|{Base}_{Y}\| \leftrightarrow 2_{𝑜} ≼ {Base}_{Y})$
23	20 21 22	mp2an	$⊢ \|2_{𝑜}\| \leq \|{Base}_{Y}\| \leftrightarrow 2_{𝑜} ≼ {Base}_{Y}$
24	17 23	sylib	$⊢ N \in ℙ \to 2_{𝑜} ≼ {Base}_{Y}$
25	13	isnzr2	$⊢ Y \in NzRing \leftrightarrow (Y \in Ring \land 2_{𝑜} ≼ {Base}_{Y})$
26	8 24 25	sylanbrc	$⊢ N \in ℙ \to Y \in NzRing$
27		eqid	$⊢ ℤRHom (Y) = ℤRHom (Y)$
28	1 13 27	znzrhfo	$⊢ N \in ℕ_{0} \to ℤRHom (Y) : ℤ \underset{onto}{⟶} {Base}_{Y}$
29	4 28	syl	$⊢ N \in ℙ \to ℤRHom (Y) : ℤ \underset{onto}{⟶} {Base}_{Y}$
30		foelrn	$⊢ (ℤRHom (Y) : ℤ \underset{onto}{⟶} {Base}_{Y} \land x \in {Base}_{Y}) \to \exists z \in ℤ x = ℤRHom (Y) (z)$
31		foelrn	$⊢ (ℤRHom (Y) : ℤ \underset{onto}{⟶} {Base}_{Y} \land y \in {Base}_{Y}) \to \exists w \in ℤ y = ℤRHom (Y) (w)$
32	30 31	anim12dan	$⊢ (ℤRHom (Y) : ℤ \underset{onto}{⟶} {Base}_{Y} \land (x \in {Base}_{Y} \land y \in {Base}_{Y})) \to (\exists z \in ℤ x = ℤRHom (Y) (z) \land \exists w \in ℤ y = ℤRHom (Y) (w))$
33	29 32	sylan	$⊢ (N \in ℙ \land (x \in {Base}_{Y} \land y \in {Base}_{Y})) \to (\exists z \in ℤ x = ℤRHom (Y) (z) \land \exists w \in ℤ y = ℤRHom (Y) (w))$
34		reeanv	$⊢ \exists z \in ℤ \exists w \in ℤ (x = ℤRHom (Y) (z) \land y = ℤRHom (Y) (w)) \leftrightarrow (\exists z \in ℤ x = ℤRHom (Y) (z) \land \exists w \in ℤ y = ℤRHom (Y) (w))$
35		euclemma	$⊢ (N \in ℙ \land z \in ℤ \land w \in ℤ) \to (N ∥ z w \leftrightarrow (N ∥ z \lor N ∥ w))$
36	35	3expb	$⊢ (N \in ℙ \land (z \in ℤ \land w \in ℤ)) \to (N ∥ z w \leftrightarrow (N ∥ z \lor N ∥ w))$
37	8	adantr	$⊢ (N \in ℙ \land (z \in ℤ \land w \in ℤ)) \to Y \in Ring$
38	27	zrhrhm	$⊢ Y \in Ring \to ℤRHom (Y) \in (ℤ_{ring} RingHom Y)$
39	37 38	syl	$⊢ (N \in ℙ \land (z \in ℤ \land w \in ℤ)) \to ℤRHom (Y) \in (ℤ_{ring} RingHom Y)$
40		simprl	$⊢ (N \in ℙ \land (z \in ℤ \land w \in ℤ)) \to z \in ℤ$
41		simprr	$⊢ (N \in ℙ \land (z \in ℤ \land w \in ℤ)) \to w \in ℤ$
42		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
43		zringmulr	$⊢ \times = \cdot_{ℤ_{ring}}$
44		eqid	$⊢ \cdot_{Y} = \cdot_{Y}$
45	42 43 44	rhmmul	$⊢ (ℤRHom (Y) \in (ℤ_{ring} RingHom Y) \land z \in ℤ \land w \in ℤ) \to ℤRHom (Y) (z w) = ℤRHom (Y) (z) \cdot_{Y} ℤRHom (Y) (w)$
46	39 40 41 45	syl3anc	$⊢ (N \in ℙ \land (z \in ℤ \land w \in ℤ)) \to ℤRHom (Y) (z w) = ℤRHom (Y) (z) \cdot_{Y} ℤRHom (Y) (w)$
47	46	eqeq1d	$⊢ (N \in ℙ \land (z \in ℤ \land w \in ℤ)) \to (ℤRHom (Y) (z w) = 0_{Y} \leftrightarrow ℤRHom (Y) (z) \cdot_{Y} ℤRHom (Y) (w) = 0_{Y})$
48		zmulcl	$⊢ (z \in ℤ \land w \in ℤ) \to z w \in ℤ$
49		eqid	$⊢ 0_{Y} = 0_{Y}$
50	1 27 49	zndvds0	$⊢ (N \in ℕ_{0} \land z w \in ℤ) \to (ℤRHom (Y) (z w) = 0_{Y} \leftrightarrow N ∥ z w)$
51	4 48 50	syl2an	$⊢ (N \in ℙ \land (z \in ℤ \land w \in ℤ)) \to (ℤRHom (Y) (z w) = 0_{Y} \leftrightarrow N ∥ z w)$
52	47 51	bitr3d	$⊢ (N \in ℙ \land (z \in ℤ \land w \in ℤ)) \to (ℤRHom (Y) (z) \cdot_{Y} ℤRHom (Y) (w) = 0_{Y} \leftrightarrow N ∥ z w)$
53	1 27 49	zndvds0	$⊢ (N \in ℕ_{0} \land z \in ℤ) \to (ℤRHom (Y) (z) = 0_{Y} \leftrightarrow N ∥ z)$
54	4 40 53	syl2an2r	$⊢ (N \in ℙ \land (z \in ℤ \land w \in ℤ)) \to (ℤRHom (Y) (z) = 0_{Y} \leftrightarrow N ∥ z)$
55	1 27 49	zndvds0	$⊢ (N \in ℕ_{0} \land w \in ℤ) \to (ℤRHom (Y) (w) = 0_{Y} \leftrightarrow N ∥ w)$
56	4 41 55	syl2an2r	$⊢ (N \in ℙ \land (z \in ℤ \land w \in ℤ)) \to (ℤRHom (Y) (w) = 0_{Y} \leftrightarrow N ∥ w)$
57	54 56	orbi12d	$⊢ (N \in ℙ \land (z \in ℤ \land w \in ℤ)) \to ((ℤRHom (Y) (z) = 0_{Y} \lor ℤRHom (Y) (w) = 0_{Y}) \leftrightarrow (N ∥ z \lor N ∥ w))$
58	36 52 57	3bitr4d	$⊢ (N \in ℙ \land (z \in ℤ \land w \in ℤ)) \to (ℤRHom (Y) (z) \cdot_{Y} ℤRHom (Y) (w) = 0_{Y} \leftrightarrow (ℤRHom (Y) (z) = 0_{Y} \lor ℤRHom (Y) (w) = 0_{Y}))$
59	58	biimpd	$⊢ (N \in ℙ \land (z \in ℤ \land w \in ℤ)) \to (ℤRHom (Y) (z) \cdot_{Y} ℤRHom (Y) (w) = 0_{Y} \to (ℤRHom (Y) (z) = 0_{Y} \lor ℤRHom (Y) (w) = 0_{Y}))$
60		oveq12	$⊢ (x = ℤRHom (Y) (z) \land y = ℤRHom (Y) (w)) \to x \cdot_{Y} y = ℤRHom (Y) (z) \cdot_{Y} ℤRHom (Y) (w)$
61	60	eqeq1d	$⊢ (x = ℤRHom (Y) (z) \land y = ℤRHom (Y) (w)) \to (x \cdot_{Y} y = 0_{Y} \leftrightarrow ℤRHom (Y) (z) \cdot_{Y} ℤRHom (Y) (w) = 0_{Y})$
62		eqeq1	$⊢ x = ℤRHom (Y) (z) \to (x = 0_{Y} \leftrightarrow ℤRHom (Y) (z) = 0_{Y})$
63	62	orbi1d	$⊢ x = ℤRHom (Y) (z) \to ((x = 0_{Y} \lor y = 0_{Y}) \leftrightarrow (ℤRHom (Y) (z) = 0_{Y} \lor y = 0_{Y}))$
64		eqeq1	$⊢ y = ℤRHom (Y) (w) \to (y = 0_{Y} \leftrightarrow ℤRHom (Y) (w) = 0_{Y})$
65	64	orbi2d	$⊢ y = ℤRHom (Y) (w) \to ((ℤRHom (Y) (z) = 0_{Y} \lor y = 0_{Y}) \leftrightarrow (ℤRHom (Y) (z) = 0_{Y} \lor ℤRHom (Y) (w) = 0_{Y}))$
66	63 65	sylan9bb	$⊢ (x = ℤRHom (Y) (z) \land y = ℤRHom (Y) (w)) \to ((x = 0_{Y} \lor y = 0_{Y}) \leftrightarrow (ℤRHom (Y) (z) = 0_{Y} \lor ℤRHom (Y) (w) = 0_{Y}))$
67	61 66	imbi12d	$⊢ (x = ℤRHom (Y) (z) \land y = ℤRHom (Y) (w)) \to ((x \cdot_{Y} y = 0_{Y} \to (x = 0_{Y} \lor y = 0_{Y})) \leftrightarrow (ℤRHom (Y) (z) \cdot_{Y} ℤRHom (Y) (w) = 0_{Y} \to (ℤRHom (Y) (z) = 0_{Y} \lor ℤRHom (Y) (w) = 0_{Y})))$
68	59 67	syl5ibrcom	$⊢ (N \in ℙ \land (z \in ℤ \land w \in ℤ)) \to ((x = ℤRHom (Y) (z) \land y = ℤRHom (Y) (w)) \to (x \cdot_{Y} y = 0_{Y} \to (x = 0_{Y} \lor y = 0_{Y})))$
69	68	rexlimdvva	$⊢ N \in ℙ \to (\exists z \in ℤ \exists w \in ℤ (x = ℤRHom (Y) (z) \land y = ℤRHom (Y) (w)) \to (x \cdot_{Y} y = 0_{Y} \to (x = 0_{Y} \lor y = 0_{Y})))$
70	34 69	syl5bir	$⊢ N \in ℙ \to ((\exists z \in ℤ x = ℤRHom (Y) (z) \land \exists w \in ℤ y = ℤRHom (Y) (w)) \to (x \cdot_{Y} y = 0_{Y} \to (x = 0_{Y} \lor y = 0_{Y})))$
71	70	imp	$⊢ (N \in ℙ \land (\exists z \in ℤ x = ℤRHom (Y) (z) \land \exists w \in ℤ y = ℤRHom (Y) (w))) \to (x \cdot_{Y} y = 0_{Y} \to (x = 0_{Y} \lor y = 0_{Y}))$
72	33 71	syldan	$⊢ (N \in ℙ \land (x \in {Base}_{Y} \land y \in {Base}_{Y})) \to (x \cdot_{Y} y = 0_{Y} \to (x = 0_{Y} \lor y = 0_{Y}))$
73	72	ralrimivva	$⊢ N \in ℙ \to \forall x \in {Base}_{Y} \forall y \in {Base}_{Y} (x \cdot_{Y} y = 0_{Y} \to (x = 0_{Y} \lor y = 0_{Y}))$
74	13 44 49	isdomn	$⊢ Y \in Domn \leftrightarrow (Y \in NzRing \land \forall x \in {Base}_{Y} \forall y \in {Base}_{Y} (x \cdot_{Y} y = 0_{Y} \to (x = 0_{Y} \lor y = 0_{Y})))$
75	26 73 74	sylanbrc	$⊢ N \in ℙ \to Y \in Domn$
76		isidom	$⊢ Y \in IDomn \leftrightarrow (Y \in CRing \land Y \in Domn)$
77	6 75 76	sylanbrc	$⊢ N \in ℙ \to Y \in IDomn$
78	1 13	znfi	$⊢ N \in ℕ \to {Base}_{Y} \in Fin$
79	2 78	syl	$⊢ N \in ℙ \to {Base}_{Y} \in Fin$
80	13	fiidomfld	$⊢ {Base}_{Y} \in Fin \to (Y \in IDomn \leftrightarrow Y \in Field)$
81	79 80	syl	$⊢ N \in ℙ \to (Y \in IDomn \leftrightarrow Y \in Field)$
82	77 81	mpbid	$⊢ N \in ℙ \to Y \in Field$

Metamath Proof Explorer

Theorem znfld

Proof