Metamath Proof Explorer

Theorem zringidom

Description: The ring of integers is an integral domain. (Contributed by Thierry Arnoux, 4-May-2025)

Ref Expression
Assertion zringidom 
|- ZZring e. IDomn

Proof

Step Hyp Ref Expression
1 zringcrng 
 |-  ZZring e. CRing
2 zringnzr 
 |-  ZZring e. NzRing
3 eldifi 
 |-  ( x e. ( ZZ \ { 0 } ) -> x e. ZZ )
4 3 ad2antrr 
 |-  ( ( ( x e. ( ZZ \ { 0 } ) /\ y e. ZZ ) /\ ( x x. y ) = 0 ) -> x e. ZZ )
5 4 zcnd 
 |-  ( ( ( x e. ( ZZ \ { 0 } ) /\ y e. ZZ ) /\ ( x x. y ) = 0 ) -> x e. CC )
6 simplr 
 |-  ( ( ( x e. ( ZZ \ { 0 } ) /\ y e. ZZ ) /\ ( x x. y ) = 0 ) -> y e. ZZ )
7 6 zcnd 
 |-  ( ( ( x e. ( ZZ \ { 0 } ) /\ y e. ZZ ) /\ ( x x. y ) = 0 ) -> y e. CC )
8 simpr 
 |-  ( ( ( x e. ( ZZ \ { 0 } ) /\ y e. ZZ ) /\ ( x x. y ) = 0 ) -> ( x x. y ) = 0 )
9 mul0or 
 |-  ( ( x e. CC /\ y e. CC ) -> ( ( x x. y ) = 0 <-> ( x = 0 \/ y = 0 ) ) )
10 9 biimpa 
 |-  ( ( ( x e. CC /\ y e. CC ) /\ ( x x. y ) = 0 ) -> ( x = 0 \/ y = 0 ) )
11 5 7 8 10 syl21anc 
 |-  ( ( ( x e. ( ZZ \ { 0 } ) /\ y e. ZZ ) /\ ( x x. y ) = 0 ) -> ( x = 0 \/ y = 0 ) )
12 eldifsni 
 |-  ( x e. ( ZZ \ { 0 } ) -> x =/= 0 )
13 12 ad2antrr 
 |-  ( ( ( x e. ( ZZ \ { 0 } ) /\ y e. ZZ ) /\ ( x x. y ) = 0 ) -> x =/= 0 )
14 13 neneqd 
 |-  ( ( ( x e. ( ZZ \ { 0 } ) /\ y e. ZZ ) /\ ( x x. y ) = 0 ) -> -. x = 0 )
15 11 14 orcnd 
 |-  ( ( ( x e. ( ZZ \ { 0 } ) /\ y e. ZZ ) /\ ( x x. y ) = 0 ) -> y = 0 )
16 15 ex 
 |-  ( ( x e. ( ZZ \ { 0 } ) /\ y e. ZZ ) -> ( ( x x. y ) = 0 -> y = 0 ) )
17 16 ralrimiva 
 |-  ( x e. ( ZZ \ { 0 } ) -> A. y e. ZZ ( ( x x. y ) = 0 -> y = 0 ) )
18 eqid 
 |-  ( RLReg ` ZZring ) = ( RLReg ` ZZring )
19 zringbas 
 |-  ZZ = ( Base ` ZZring )
20 zringmulr 
 |-  x. = ( .r ` ZZring )
21 zring0 
 |-  0 = ( 0g ` ZZring )
22 18 19 20 21 isrrg 
 |-  ( x e. ( RLReg ` ZZring ) <-> ( x e. ZZ /\ A. y e. ZZ ( ( x x. y ) = 0 -> y = 0 ) ) )
23 3 17 22 sylanbrc 
 |-  ( x e. ( ZZ \ { 0 } ) -> x e. ( RLReg ` ZZring ) )
24 23 ssriv 
 |-  ( ZZ \ { 0 } ) C_ ( RLReg ` ZZring )
25 19 18 21 isdomn2 
 |-  ( ZZring e. Domn <-> ( ZZring e. NzRing /\ ( ZZ \ { 0 } ) C_ ( RLReg ` ZZring ) ) )
26 2 24 25 mpbir2an 
 |-  ZZring e. Domn
27 isidom 
 |-  ( ZZring e. IDomn <-> ( ZZring e. CRing /\ ZZring e. Domn ) )
28 1 26 27 mpbir2an 
 |-  ZZring e. IDomn