Metamath Proof Explorer

Theorem zringpid

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

Ref Expression
Assertion zringpid 
|- ZZring e. PID

Proof

Step Hyp Ref Expression
1 zringidom 
 |-  ZZring e. IDomn
2 zringlpir 
 |-  ZZring e. LPIR
3 1 2 elini 
 |-  ZZring e. ( IDomn i^i LPIR )
4 df-pid 
 |-  PID = ( IDomn i^i LPIR )
5 3 4 eleqtrri 
 |-  ZZring e. PID