Theorem zringlpir

Description: The integers are a principal ideal ring. (Contributed by Stefan O'Rear, 3-Jan-2015) (Revised by AV, 9-Jun-2019) (Proof shortened by AV, 27-Sep-2020)

	Ref	Expression
Assertion	zringlpir	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{LPIR}$$

Proof

Step	Hyp	Ref	Expression
1		zringring	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}$$
2		eleq1	$$⊢x=\left\{0\right\}\to \left(x\in \mathrm{LPIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\leftrightarrow \left\{0\right\}\in \mathrm{LPIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\right)$$
3		simpl	$$⊢\left(x\in \mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\wedge x\ne \left\{0\right\}\right)\to x\in \mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
4		simpr	$$⊢\left(x\in \mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\wedge x\ne \left\{0\right\}\right)\to x\ne \left\{0\right\}$$
5		eqid	$$⊢inf\left(x\cap \mathbb{N},ℝ,<\right)=inf\left(x\cap \mathbb{N},ℝ,<\right)$$
6	3 4 5	zringlpirlem2	$$⊢\left(x\in \mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\wedge x\ne \left\{0\right\}\right)\to inf\left(x\cap \mathbb{N},ℝ,<\right)\in x$$
7		simpll	$$⊢\left(\left(x\in \mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\wedge x\ne \left\{0\right\}\right)\wedge z\in x\right)\to x\in \mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
8		simplr	$$⊢\left(\left(x\in \mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\wedge x\ne \left\{0\right\}\right)\wedge z\in x\right)\to x\ne \left\{0\right\}$$
9		simpr	$$⊢\left(\left(x\in \mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\wedge x\ne \left\{0\right\}\right)\wedge z\in x\right)\to z\in x$$
10	7 8 5 9	zringlpirlem3	$$⊢\left(\left(x\in \mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\wedge x\ne \left\{0\right\}\right)\wedge z\in x\right)\to inf\left(x\cap \mathbb{N},ℝ,<\right)\parallel z$$
11	10	ralrimiva	$$⊢\left(x\in \mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\wedge x\ne \left\{0\right\}\right)\to \forall z\in xinf\left(x\cap \mathbb{N},ℝ,<\right)\parallel z$$
12		breq1	$$⊢y=inf\left(x\cap \mathbb{N},ℝ,<\right)\to \left(y\parallel z\leftrightarrow inf\left(x\cap \mathbb{N},ℝ,<\right)\parallel z\right)$$
13	12	ralbidv	$$⊢y=inf\left(x\cap \mathbb{N},ℝ,<\right)\to \left(\forall z\in xy\parallel z\leftrightarrow \forall z\in xinf\left(x\cap \mathbb{N},ℝ,<\right)\parallel z\right)$$
14	13	rspcev	$$⊢\left(inf\left(x\cap \mathbb{N},ℝ,<\right)\in x\wedge \forall z\in xinf\left(x\cap \mathbb{N},ℝ,<\right)\parallel z\right)\to \exists y\in x\forall z\in xy\parallel z$$
15	6 11 14	syl2anc	$$⊢\left(x\in \mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\wedge x\ne \left\{0\right\}\right)\to \exists y\in x\forall z\in xy\parallel z$$
16		eqid	$$⊢\mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)=\mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
17		eqid	$$⊢\mathrm{LPIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)=\mathrm{LPIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
18		dvdsrzring	$$⊢\parallel ={\parallel }_r\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
19	16 17 18	lpigen	$$⊢\left({\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}\wedge x\in \mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\right)\to \left(x\in \mathrm{LPIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\leftrightarrow \exists y\in x\forall z\in xy\parallel z\right)$$
20	1 19	mpan	$$⊢x\in \mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\to \left(x\in \mathrm{LPIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\leftrightarrow \exists y\in x\forall z\in xy\parallel z\right)$$
21	20	adantr	$$⊢\left(x\in \mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\wedge x\ne \left\{0\right\}\right)\to \left(x\in \mathrm{LPIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\leftrightarrow \exists y\in x\forall z\in xy\parallel z\right)$$
22	15 21	mpbird	$$⊢\left(x\in \mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\wedge x\ne \left\{0\right\}\right)\to x\in \mathrm{LPIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
23		zring0	$$⊢0=0_{{\mathbb{Z}}_{\mathrm{ring}}}$$
24	17 23	lpi0	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}\to \left\{0\right\}\in \mathrm{LPIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
25	1 24	mp1i	$$⊢x\in \mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\to \left\{0\right\}\in \mathrm{LPIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
26	2 22 25	pm2.61ne	$$⊢x\in \mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\to x\in \mathrm{LPIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
27	26	ssriv	$$⊢\mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\subseteq \mathrm{LPIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
28	17 16	islpir2	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{LPIR}\leftrightarrow \left({\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}\wedge \mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\subseteq \mathrm{LPIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\right)$$
29	1 27 28	mpbir2an	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{LPIR}$$