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 = ℤ / N ℤ$
	Assertion	znidomb	$⊢ N \in ℕ \to (Y \in IDomn \leftrightarrow N \in ℙ)$

Proof

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

Metamath Proof Explorer

Theorem znidomb

Proof