Theorem zringpid

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

	Ref	Expression
Assertion	zringpid	⊢ ℤring ∈ PID

Proof

Step	Hyp	Ref	Expression
1		zringidom	⊢ ℤring ∈ IDomn
2		zringlpir	⊢ ℤring ∈ LPIR
3	1 2	elini	⊢ ℤring ∈ ( IDomn ∩ LPIR )
4		df-pid	⊢ PID = ( IDomn ∩ LPIR )
5	3 4	eleqtrri	⊢ ℤring ∈ PID