Theorem prmirred

Description: The irreducible elements of ZZ are exactly the prime numbers (and their negatives). (Contributed by Mario Carneiro, 5-Dec-2014) (Revised by AV, 10-Jun-2019)

	Ref	Expression
Hypothesis	prmirred.i	$$⊢I=\mathrm{Irred}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
Assertion	prmirred	$$⊢A\in I\leftrightarrow \left(A\in \mathbb{Z}\wedge \left|A\right|\in \mathbb{P}\right)$$

Proof

Step	Hyp	Ref	Expression
1		prmirred.i	$$⊢I=\mathrm{Irred}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
2		zringbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
3	1 2	irredcl	$$⊢A\in I\to A\in \mathbb{Z}$$
4		elnn0	$$⊢A\in {\mathbb{N}}_0\leftrightarrow \left(A\in \mathbb{N}\vee A=0\right)$$
5		zringring	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}$$
6		zring0	$$⊢0=0_{{\mathbb{Z}}_{\mathrm{ring}}}$$
7	1 6	irredn0	$$⊢\left({\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}\wedge A\in I\right)\to A\ne 0$$
8	5 7	mpan	$$⊢A\in I\to A\ne 0$$
9	8	necon2bi	$$⊢A=0\to \neg A\in I$$
10	9	pm2.21d	$$⊢A=0\to \left(A\in I\to A\in \mathbb{N}\right)$$
11	10	jao1i	$$⊢\left(A\in \mathbb{N}\vee A=0\right)\to \left(A\in I\to A\in \mathbb{N}\right)$$
12	4 11	sylbi	$$⊢A\in {\mathbb{N}}_0\to \left(A\in I\to A\in \mathbb{N}\right)$$
13		prmnn	$$⊢A\in \mathbb{P}\to A\in \mathbb{N}$$
14	13	a1i	$$⊢A\in {\mathbb{N}}_0\to \left(A\in \mathbb{P}\to A\in \mathbb{N}\right)$$
15	1	prmirredlem	$$⊢A\in \mathbb{N}\to \left(A\in I\leftrightarrow A\in \mathbb{P}\right)$$
16	15	a1i	$$⊢A\in {\mathbb{N}}_0\to \left(A\in \mathbb{N}\to \left(A\in I\leftrightarrow A\in \mathbb{P}\right)\right)$$
17	12 14 16	pm5.21ndd	$$⊢A\in {\mathbb{N}}_0\to \left(A\in I\leftrightarrow A\in \mathbb{P}\right)$$
18		nn0re	$$⊢A\in {\mathbb{N}}_0\to A\in ℝ$$
19		nn0ge0	$$⊢A\in {\mathbb{N}}_0\to 0\le A$$
20	18 19	absidd	$$⊢A\in {\mathbb{N}}_0\to \left|A\right|=A$$
21	20	eleq1d	$$⊢A\in {\mathbb{N}}_0\to \left(\left|A\right|\in \mathbb{P}\leftrightarrow A\in \mathbb{P}\right)$$
22	17 21	bitr4d	$$⊢A\in {\mathbb{N}}_0\to \left(A\in I\leftrightarrow \left|A\right|\in \mathbb{P}\right)$$
23	22	adantl	$$⊢\left(A\in \mathbb{Z}\wedge A\in {\mathbb{N}}_0\right)\to \left(A\in I\leftrightarrow \left|A\right|\in \mathbb{P}\right)$$
24	1	prmirredlem	$$⊢-A\in \mathbb{N}\to \left(-A\in I\leftrightarrow -A\in \mathbb{P}\right)$$
25	24	adantl	$$⊢\left(A\in \mathbb{Z}\wedge -A\in \mathbb{N}\right)\to \left(-A\in I\leftrightarrow -A\in \mathbb{P}\right)$$
26		eqid	$$⊢{inv}_g\left({\mathbb{Z}}_{\mathrm{ring}}\right)={inv}_g\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
27	1 26 2	irrednegb	$$⊢\left({\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}\wedge A\in \mathbb{Z}\right)\to \left(A\in I\leftrightarrow {inv}_g\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(A\right)\in I\right)$$
28	5 27	mpan	$$⊢A\in \mathbb{Z}\to \left(A\in I\leftrightarrow {inv}_g\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(A\right)\in I\right)$$
29		zsubrg	$$⊢\mathbb{Z}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
30		subrgsubg	$$⊢\mathbb{Z}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to \mathbb{Z}\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)$$
31	29 30	ax-mp	$$⊢\mathbb{Z}\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)$$
32		df-zring	$$⊢{\mathbb{Z}}_{\mathrm{ring}}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}$$
33		eqid	$$⊢{inv}_g\left({ℂ}_{\mathrm{fld}}\right)={inv}_g\left({ℂ}_{\mathrm{fld}}\right)$$
34	32 33 26	subginv	$$⊢\left(\mathbb{Z}\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)\wedge A\in \mathbb{Z}\right)\to {inv}_g\left({ℂ}_{\mathrm{fld}}\right)\left(A\right)={inv}_g\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(A\right)$$
35	31 34	mpan	$$⊢A\in \mathbb{Z}\to {inv}_g\left({ℂ}_{\mathrm{fld}}\right)\left(A\right)={inv}_g\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(A\right)$$
36		zcn	$$⊢A\in \mathbb{Z}\to A\in ℂ$$
37		cnfldneg	$$⊢A\in ℂ\to {inv}_g\left({ℂ}_{\mathrm{fld}}\right)\left(A\right)=-A$$
38	36 37	syl	$$⊢A\in \mathbb{Z}\to {inv}_g\left({ℂ}_{\mathrm{fld}}\right)\left(A\right)=-A$$
39	35 38	eqtr3d	$$⊢A\in \mathbb{Z}\to {inv}_g\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(A\right)=-A$$
40	39	eleq1d	$$⊢A\in \mathbb{Z}\to \left({inv}_g\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(A\right)\in I\leftrightarrow -A\in I\right)$$
41	28 40	bitrd	$$⊢A\in \mathbb{Z}\to \left(A\in I\leftrightarrow -A\in I\right)$$
42	41	adantr	$$⊢\left(A\in \mathbb{Z}\wedge -A\in \mathbb{N}\right)\to \left(A\in I\leftrightarrow -A\in I\right)$$
43		zre	$$⊢A\in \mathbb{Z}\to A\in ℝ$$
44	43	adantr	$$⊢\left(A\in \mathbb{Z}\wedge -A\in \mathbb{N}\right)\to A\in ℝ$$
45		nnnn0	$$⊢-A\in \mathbb{N}\to -A\in {\mathbb{N}}_0$$
46	45	nn0ge0d	$$⊢-A\in \mathbb{N}\to 0\le -A$$
47	46	adantl	$$⊢\left(A\in \mathbb{Z}\wedge -A\in \mathbb{N}\right)\to 0\le -A$$
48	44	le0neg1d	$$⊢\left(A\in \mathbb{Z}\wedge -A\in \mathbb{N}\right)\to \left(A\le 0\leftrightarrow 0\le -A\right)$$
49	47 48	mpbird	$$⊢\left(A\in \mathbb{Z}\wedge -A\in \mathbb{N}\right)\to A\le 0$$
50	44 49	absnidd	$$⊢\left(A\in \mathbb{Z}\wedge -A\in \mathbb{N}\right)\to \left|A\right|=-A$$
51	50	eleq1d	$$⊢\left(A\in \mathbb{Z}\wedge -A\in \mathbb{N}\right)\to \left(\left|A\right|\in \mathbb{P}\leftrightarrow -A\in \mathbb{P}\right)$$
52	25 42 51	3bitr4d	$$⊢\left(A\in \mathbb{Z}\wedge -A\in \mathbb{N}\right)\to \left(A\in I\leftrightarrow \left|A\right|\in \mathbb{P}\right)$$
53	52	adantrl	$$⊢\left(A\in \mathbb{Z}\wedge \left(A\in ℝ\wedge -A\in \mathbb{N}\right)\right)\to \left(A\in I\leftrightarrow \left|A\right|\in \mathbb{P}\right)$$
54		elznn0nn	$$⊢A\in \mathbb{Z}\leftrightarrow \left(A\in {\mathbb{N}}_0\vee \left(A\in ℝ\wedge -A\in \mathbb{N}\right)\right)$$
55	54	biimpi	$$⊢A\in \mathbb{Z}\to \left(A\in {\mathbb{N}}_0\vee \left(A\in ℝ\wedge -A\in \mathbb{N}\right)\right)$$
56	23 53 55	mpjaodan	$$⊢A\in \mathbb{Z}\to \left(A\in I\leftrightarrow \left|A\right|\in \mathbb{P}\right)$$
57	3 56	biadanii	$$⊢A\in I\leftrightarrow \left(A\in \mathbb{Z}\wedge \left|A\right|\in \mathbb{P}\right)$$