Theorem zringpid

Description: The ring of integers is a principal ideal domain. (Contributed by Thierry Arnoux, 18-May-2025)

	Ref	Expression
Assertion	zringpid	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{PID}$$

Proof

Step	Hyp	Ref	Expression
1		zringidom	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{IDomn}$$
2		zringlpir	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{LPIR}$$
3	1 2	elini	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \left(\mathrm{IDomn}\cap \mathrm{LPIR}\right)$$
4		df-pid	$$⊢\mathrm{PID}=\mathrm{IDomn}\cap \mathrm{LPIR}$$
5	3 4	eleqtrri	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{PID}$$