prmirredlem

Description: A positive integer is irreducible over ZZ iff it is a prime number. (Contributed by Mario Carneiro, 5-Dec-2014) (Revised by AV, 10-Jun-2019)

		Ref	Expression
	Hypothesis	prmirred.i	$⊢ I = Irred (ℤ_{ring})$
	Assertion	prmirredlem	$⊢ A \in ℕ \to (A \in I \leftrightarrow A \in ℙ)$

Proof

Step	Hyp	Ref	Expression
1		prmirred.i	$⊢ I = Irred (ℤ_{ring})$
2		zringring	$⊢ ℤ_{ring} \in Ring$
3		zring1	$⊢ 1 = 1_{ℤ_{ring}}$
4	1 3	irredn1	$⊢ (ℤ_{ring} \in Ring \land A \in I) \to A \neq 1$
5	2 4	mpan	$⊢ A \in I \to A \neq 1$
6	5	anim2i	$⊢ (A \in ℕ \land A \in I) \to (A \in ℕ \land A \neq 1)$
7		eluz2b3	$⊢ A \in ℤ_{\geq 2} \leftrightarrow (A \in ℕ \land A \neq 1)$
8	6 7	sylibr	$⊢ (A \in ℕ \land A \in I) \to A \in ℤ_{\geq 2}$
9		nnz	$⊢ y \in ℕ \to y \in ℤ$
10	9	ad2antrl	$⊢ ((A \in ℕ \land A \in I) \land (y \in ℕ \land y ∥ A)) \to y \in ℤ$
11		simprr	$⊢ ((A \in ℕ \land A \in I) \land (y \in ℕ \land y ∥ A)) \to y ∥ A$
12		nnne0	$⊢ y \in ℕ \to y \neq 0$
13	12	ad2antrl	$⊢ ((A \in ℕ \land A \in I) \land (y \in ℕ \land y ∥ A)) \to y \neq 0$
14		nnz	$⊢ A \in ℕ \to A \in ℤ$
15	14	ad2antrr	$⊢ ((A \in ℕ \land A \in I) \land (y \in ℕ \land y ∥ A)) \to A \in ℤ$
16		dvdsval2	$⊢ (y \in ℤ \land y \neq 0 \land A \in ℤ) \to (y ∥ A \leftrightarrow \frac{A}{y} \in ℤ)$
17	10 13 15 16	syl3anc	$⊢ ((A \in ℕ \land A \in I) \land (y \in ℕ \land y ∥ A)) \to (y ∥ A \leftrightarrow \frac{A}{y} \in ℤ)$
18	11 17	mpbid	$⊢ ((A \in ℕ \land A \in I) \land (y \in ℕ \land y ∥ A)) \to \frac{A}{y} \in ℤ$
19	15	zcnd	$⊢ ((A \in ℕ \land A \in I) \land (y \in ℕ \land y ∥ A)) \to A \in ℂ$
20		nncn	$⊢ y \in ℕ \to y \in ℂ$
21	20	ad2antrl	$⊢ ((A \in ℕ \land A \in I) \land (y \in ℕ \land y ∥ A)) \to y \in ℂ$
22	19 21 13	divcan2d	$⊢ ((A \in ℕ \land A \in I) \land (y \in ℕ \land y ∥ A)) \to y (\frac{A}{y}) = A$
23		simplr	$⊢ ((A \in ℕ \land A \in I) \land (y \in ℕ \land y ∥ A)) \to A \in I$
24	22 23	eqeltrd	$⊢ ((A \in ℕ \land A \in I) \land (y \in ℕ \land y ∥ A)) \to y (\frac{A}{y}) \in I$
25		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
26		eqid	$⊢ Unit (ℤ_{ring}) = Unit (ℤ_{ring})$
27		zringmulr	$⊢ \times = \cdot_{ℤ_{ring}}$
28	1 25 26 27	irredmul	$⊢ (y \in ℤ \land \frac{A}{y} \in ℤ \land y (\frac{A}{y}) \in I) \to (y \in Unit (ℤ_{ring}) \lor \frac{A}{y} \in Unit (ℤ_{ring}))$
29	10 18 24 28	syl3anc	$⊢ ((A \in ℕ \land A \in I) \land (y \in ℕ \land y ∥ A)) \to (y \in Unit (ℤ_{ring}) \lor \frac{A}{y} \in Unit (ℤ_{ring}))$
30		zringunit	$⊢ y \in Unit (ℤ_{ring}) \leftrightarrow (y \in ℤ \land \|y\| = 1)$
31	30	baib	$⊢ y \in ℤ \to (y \in Unit (ℤ_{ring}) \leftrightarrow \|y\| = 1)$
32	10 31	syl	$⊢ ((A \in ℕ \land A \in I) \land (y \in ℕ \land y ∥ A)) \to (y \in Unit (ℤ_{ring}) \leftrightarrow \|y\| = 1)$
33		nnnn0	$⊢ y \in ℕ \to y \in ℕ_{0}$
34		nn0re	$⊢ y \in ℕ_{0} \to y \in ℝ$
35		nn0ge0	$⊢ y \in ℕ_{0} \to 0 \leq y$
36	34 35	absidd	$⊢ y \in ℕ_{0} \to \|y\| = y$
37	33 36	syl	$⊢ y \in ℕ \to \|y\| = y$
38	37	ad2antrl	$⊢ ((A \in ℕ \land A \in I) \land (y \in ℕ \land y ∥ A)) \to \|y\| = y$
39	38	eqeq1d	$⊢ ((A \in ℕ \land A \in I) \land (y \in ℕ \land y ∥ A)) \to (\|y\| = 1 \leftrightarrow y = 1)$
40	32 39	bitrd	$⊢ ((A \in ℕ \land A \in I) \land (y \in ℕ \land y ∥ A)) \to (y \in Unit (ℤ_{ring}) \leftrightarrow y = 1)$
41		zringunit	$⊢ \frac{A}{y} \in Unit (ℤ_{ring}) \leftrightarrow (\frac{A}{y} \in ℤ \land \|\frac{A}{y}\| = 1)$
42	41	baib	$⊢ \frac{A}{y} \in ℤ \to (\frac{A}{y} \in Unit (ℤ_{ring}) \leftrightarrow \|\frac{A}{y}\| = 1)$
43	18 42	syl	$⊢ ((A \in ℕ \land A \in I) \land (y \in ℕ \land y ∥ A)) \to (\frac{A}{y} \in Unit (ℤ_{ring}) \leftrightarrow \|\frac{A}{y}\| = 1)$
44		nnre	$⊢ A \in ℕ \to A \in ℝ$
45	44	ad2antrr	$⊢ ((A \in ℕ \land A \in I) \land (y \in ℕ \land y ∥ A)) \to A \in ℝ$
46		simprl	$⊢ ((A \in ℕ \land A \in I) \land (y \in ℕ \land y ∥ A)) \to y \in ℕ$
47	45 46	nndivred	$⊢ ((A \in ℕ \land A \in I) \land (y \in ℕ \land y ∥ A)) \to \frac{A}{y} \in ℝ$
48		nnnn0	$⊢ A \in ℕ \to A \in ℕ_{0}$
49		nn0ge0	$⊢ A \in ℕ_{0} \to 0 \leq A$
50	48 49	syl	$⊢ A \in ℕ \to 0 \leq A$
51	50	ad2antrr	$⊢ ((A \in ℕ \land A \in I) \land (y \in ℕ \land y ∥ A)) \to 0 \leq A$
52	46	nnred	$⊢ ((A \in ℕ \land A \in I) \land (y \in ℕ \land y ∥ A)) \to y \in ℝ$
53		nngt0	$⊢ y \in ℕ \to 0 < y$
54	53	ad2antrl	$⊢ ((A \in ℕ \land A \in I) \land (y \in ℕ \land y ∥ A)) \to 0 < y$
55		divge0	$⊢ ((A \in ℝ \land 0 \leq A) \land (y \in ℝ \land 0 < y)) \to 0 \leq \frac{A}{y}$
56	45 51 52 54 55	syl22anc	$⊢ ((A \in ℕ \land A \in I) \land (y \in ℕ \land y ∥ A)) \to 0 \leq \frac{A}{y}$
57	47 56	absidd	$⊢ ((A \in ℕ \land A \in I) \land (y \in ℕ \land y ∥ A)) \to \|\frac{A}{y}\| = \frac{A}{y}$
58	57	eqeq1d	$⊢ ((A \in ℕ \land A \in I) \land (y \in ℕ \land y ∥ A)) \to (\|\frac{A}{y}\| = 1 \leftrightarrow \frac{A}{y} = 1)$
59		1cnd	$⊢ ((A \in ℕ \land A \in I) \land (y \in ℕ \land y ∥ A)) \to 1 \in ℂ$
60	19 21 59 13	divmuld	$⊢ ((A \in ℕ \land A \in I) \land (y \in ℕ \land y ∥ A)) \to (\frac{A}{y} = 1 \leftrightarrow y \cdot 1 = A)$
61	21	mulid1d	$⊢ ((A \in ℕ \land A \in I) \land (y \in ℕ \land y ∥ A)) \to y \cdot 1 = y$
62	61	eqeq1d	$⊢ ((A \in ℕ \land A \in I) \land (y \in ℕ \land y ∥ A)) \to (y \cdot 1 = A \leftrightarrow y = A)$
63	58 60 62	3bitrd	$⊢ ((A \in ℕ \land A \in I) \land (y \in ℕ \land y ∥ A)) \to (\|\frac{A}{y}\| = 1 \leftrightarrow y = A)$
64	43 63	bitrd	$⊢ ((A \in ℕ \land A \in I) \land (y \in ℕ \land y ∥ A)) \to (\frac{A}{y} \in Unit (ℤ_{ring}) \leftrightarrow y = A)$
65	40 64	orbi12d	$⊢ ((A \in ℕ \land A \in I) \land (y \in ℕ \land y ∥ A)) \to ((y \in Unit (ℤ_{ring}) \lor \frac{A}{y} \in Unit (ℤ_{ring})) \leftrightarrow (y = 1 \lor y = A))$
66	29 65	mpbid	$⊢ ((A \in ℕ \land A \in I) \land (y \in ℕ \land y ∥ A)) \to (y = 1 \lor y = A)$
67	66	expr	$⊢ ((A \in ℕ \land A \in I) \land y \in ℕ) \to (y ∥ A \to (y = 1 \lor y = A))$
68	67	ralrimiva	$⊢ (A \in ℕ \land A \in I) \to \forall y \in ℕ (y ∥ A \to (y = 1 \lor y = A))$
69		isprm2	$⊢ A \in ℙ \leftrightarrow (A \in ℤ_{\geq 2} \land \forall y \in ℕ (y ∥ A \to (y = 1 \lor y = A)))$
70	8 68 69	sylanbrc	$⊢ (A \in ℕ \land A \in I) \to A \in ℙ$
71		prmz	$⊢ A \in ℙ \to A \in ℤ$
72		1nprm	$⊢ \neg 1 \in ℙ$
73		zringunit	$⊢ A \in Unit (ℤ_{ring}) \leftrightarrow (A \in ℤ \land \|A\| = 1)$
74		prmnn	$⊢ A \in ℙ \to A \in ℕ$
75		nn0re	$⊢ A \in ℕ_{0} \to A \in ℝ$
76	75 49	absidd	$⊢ A \in ℕ_{0} \to \|A\| = A$
77	74 48 76	3syl	$⊢ A \in ℙ \to \|A\| = A$
78		id	$⊢ A \in ℙ \to A \in ℙ$
79	77 78	eqeltrd	$⊢ A \in ℙ \to \|A\| \in ℙ$
80		eleq1	$⊢ \|A\| = 1 \to (\|A\| \in ℙ \leftrightarrow 1 \in ℙ)$
81	79 80	syl5ibcom	$⊢ A \in ℙ \to (\|A\| = 1 \to 1 \in ℙ)$
82	81	adantld	$⊢ A \in ℙ \to ((A \in ℤ \land \|A\| = 1) \to 1 \in ℙ)$
83	73 82	syl5bi	$⊢ A \in ℙ \to (A \in Unit (ℤ_{ring}) \to 1 \in ℙ)$
84	72 83	mtoi	$⊢ A \in ℙ \to \neg A \in Unit (ℤ_{ring})$
85		dvdsmul1	$⊢ (x \in ℤ \land y \in ℤ) \to x ∥ x y$
86	85	ad2antlr	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to x ∥ x y$
87		simpr	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to x y = A$
88	86 87	breqtrd	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to x ∥ A$
89		simplrl	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to x \in ℤ$
90	71	ad2antrr	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to A \in ℤ$
91		absdvdsb	$⊢ (x \in ℤ \land A \in ℤ) \to (x ∥ A \leftrightarrow \|x\| ∥ A)$
92	89 90 91	syl2anc	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to (x ∥ A \leftrightarrow \|x\| ∥ A)$
93	88 92	mpbid	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to \|x\| ∥ A$
94		breq1	$⊢ y = \|x\| \to (y ∥ A \leftrightarrow \|x\| ∥ A)$
95		eqeq1	$⊢ y = \|x\| \to (y = 1 \leftrightarrow \|x\| = 1)$
96		eqeq1	$⊢ y = \|x\| \to (y = A \leftrightarrow \|x\| = A)$
97	95 96	orbi12d	$⊢ y = \|x\| \to ((y = 1 \lor y = A) \leftrightarrow (\|x\| = 1 \lor \|x\| = A))$
98	94 97	imbi12d	$⊢ y = \|x\| \to ((y ∥ A \to (y = 1 \lor y = A)) \leftrightarrow (\|x\| ∥ A \to (\|x\| = 1 \lor \|x\| = A)))$
99	69	simprbi	$⊢ A \in ℙ \to \forall y \in ℕ (y ∥ A \to (y = 1 \lor y = A))$
100	99	ad2antrr	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to \forall y \in ℕ (y ∥ A \to (y = 1 \lor y = A))$
101	89	zcnd	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to x \in ℂ$
102	74	ad2antrr	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to A \in ℕ$
103	102	nnne0d	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to A \neq 0$
104		simplrr	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to y \in ℤ$
105	104	zcnd	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to y \in ℂ$
106	105	mul02d	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to 0 \cdot y = 0$
107	103 87 106	3netr4d	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to x y \neq 0 \cdot y$
108		oveq1	$⊢ x = 0 \to x y = 0 \cdot y$
109	108	necon3i	$⊢ x y \neq 0 \cdot y \to x \neq 0$
110	107 109	syl	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to x \neq 0$
111	101 110	absne0d	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to \|x\| \neq 0$
112	111	neneqd	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to \neg \|x\| = 0$
113		nn0abscl	$⊢ x \in ℤ \to \|x\| \in ℕ_{0}$
114	89 113	syl	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to \|x\| \in ℕ_{0}$
115		elnn0	$⊢ \|x\| \in ℕ_{0} \leftrightarrow (\|x\| \in ℕ \lor \|x\| = 0)$
116	114 115	sylib	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to (\|x\| \in ℕ \lor \|x\| = 0)$
117	116	ord	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to (\neg \|x\| \in ℕ \to \|x\| = 0)$
118	112 117	mt3d	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to \|x\| \in ℕ$
119	98 100 118	rspcdva	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to (\|x\| ∥ A \to (\|x\| = 1 \lor \|x\| = A))$
120	93 119	mpd	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to (\|x\| = 1 \lor \|x\| = A)$
121		zringunit	$⊢ x \in Unit (ℤ_{ring}) \leftrightarrow (x \in ℤ \land \|x\| = 1)$
122	121	baib	$⊢ x \in ℤ \to (x \in Unit (ℤ_{ring}) \leftrightarrow \|x\| = 1)$
123	89 122	syl	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to (x \in Unit (ℤ_{ring}) \leftrightarrow \|x\| = 1)$
124	104 31	syl	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to (y \in Unit (ℤ_{ring}) \leftrightarrow \|y\| = 1)$
125	105	abscld	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to \|y\| \in ℝ$
126	125	recnd	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to \|y\| \in ℂ$
127		1cnd	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to 1 \in ℂ$
128	101	abscld	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to \|x\| \in ℝ$
129	128	recnd	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to \|x\| \in ℂ$
130	126 127 129 111	mulcand	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to (\|x\| \|y\| = \|x\| \cdot 1 \leftrightarrow \|y\| = 1)$
131	87	fveq2d	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to \|x y\| = \|A\|$
132	101 105	absmuld	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to \|x y\| = \|x\| \|y\|$
133	77	ad2antrr	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to \|A\| = A$
134	131 132 133	3eqtr3d	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to \|x\| \|y\| = A$
135	129	mulid1d	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to \|x\| \cdot 1 = \|x\|$
136	134 135	eqeq12d	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to (\|x\| \|y\| = \|x\| \cdot 1 \leftrightarrow A = \|x\|)$
137		eqcom	$⊢ A = \|x\| \leftrightarrow \|x\| = A$
138	136 137	bitrdi	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to (\|x\| \|y\| = \|x\| \cdot 1 \leftrightarrow \|x\| = A)$
139	124 130 138	3bitr2d	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to (y \in Unit (ℤ_{ring}) \leftrightarrow \|x\| = A)$
140	123 139	orbi12d	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to ((x \in Unit (ℤ_{ring}) \lor y \in Unit (ℤ_{ring})) \leftrightarrow (\|x\| = 1 \lor \|x\| = A))$
141	120 140	mpbird	$⊢ ((A \in ℙ \land (x \in ℤ \land y \in ℤ)) \land x y = A) \to (x \in Unit (ℤ_{ring}) \lor y \in Unit (ℤ_{ring}))$
142	141	ex	$⊢ (A \in ℙ \land (x \in ℤ \land y \in ℤ)) \to (x y = A \to (x \in Unit (ℤ_{ring}) \lor y \in Unit (ℤ_{ring})))$
143	142	ralrimivva	$⊢ A \in ℙ \to \forall x \in ℤ \forall y \in ℤ (x y = A \to (x \in Unit (ℤ_{ring}) \lor y \in Unit (ℤ_{ring})))$
144	25 26 1 27	isirred2	$⊢ A \in I \leftrightarrow (A \in ℤ \land \neg A \in Unit (ℤ_{ring}) \land \forall x \in ℤ \forall y \in ℤ (x y = A \to (x \in Unit (ℤ_{ring}) \lor y \in Unit (ℤ_{ring}))))$
145	71 84 143 144	syl3anbrc	$⊢ A \in ℙ \to A \in I$
146	145	adantl	$⊢ (A \in ℕ \land A \in ℙ) \to A \in I$
147	70 146	impbida	$⊢ A \in ℕ \to (A \in I \leftrightarrow A \in ℙ)$

Metamath Proof Explorer

Theorem prmirredlem

Proof