Theorem zringidom

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

	Ref	Expression
Assertion	zringidom	⊢ ℤring ∈ IDomn

Proof

Step	Hyp	Ref	Expression
1		zringcrng	⊢ ℤring ∈ CRing
2		zringnzr	⊢ ℤring ∈ NzRing
3		eldifi	⊢ ( 𝑥 ∈ ( ℤ ∖ { 0 } ) → 𝑥 ∈ ℤ )
4	3	ad2antrr	⊢ ( ( ( 𝑥 ∈ ( ℤ ∖ { 0 } ) ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 · 𝑦 ) = 0 ) → 𝑥 ∈ ℤ )
5	4	zcnd	⊢ ( ( ( 𝑥 ∈ ( ℤ ∖ { 0 } ) ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 · 𝑦 ) = 0 ) → 𝑥 ∈ ℂ )
6		simplr	⊢ ( ( ( 𝑥 ∈ ( ℤ ∖ { 0 } ) ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 · 𝑦 ) = 0 ) → 𝑦 ∈ ℤ )
7	6	zcnd	⊢ ( ( ( 𝑥 ∈ ( ℤ ∖ { 0 } ) ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 · 𝑦 ) = 0 ) → 𝑦 ∈ ℂ )
8		simpr	⊢ ( ( ( 𝑥 ∈ ( ℤ ∖ { 0 } ) ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 · 𝑦 ) = 0 ) → ( 𝑥 · 𝑦 ) = 0 )
9		mul0or	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 𝑥 · 𝑦 ) = 0 ↔ ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) )
10	9	biimpa	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑥 · 𝑦 ) = 0 ) → ( 𝑥 = 0 ∨ 𝑦 = 0 ) )
11	5 7 8 10	syl21anc	⊢ ( ( ( 𝑥 ∈ ( ℤ ∖ { 0 } ) ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 · 𝑦 ) = 0 ) → ( 𝑥 = 0 ∨ 𝑦 = 0 ) )
12		eldifsni	⊢ ( 𝑥 ∈ ( ℤ ∖ { 0 } ) → 𝑥 ≠ 0 )
13	12	ad2antrr	⊢ ( ( ( 𝑥 ∈ ( ℤ ∖ { 0 } ) ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 · 𝑦 ) = 0 ) → 𝑥 ≠ 0 )
14	13	neneqd	⊢ ( ( ( 𝑥 ∈ ( ℤ ∖ { 0 } ) ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 · 𝑦 ) = 0 ) → ¬ 𝑥 = 0 )
15	11 14	orcnd	⊢ ( ( ( 𝑥 ∈ ( ℤ ∖ { 0 } ) ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 · 𝑦 ) = 0 ) → 𝑦 = 0 )
16	15	ex	⊢ ( ( 𝑥 ∈ ( ℤ ∖ { 0 } ) ∧ 𝑦 ∈ ℤ ) → ( ( 𝑥 · 𝑦 ) = 0 → 𝑦 = 0 ) )
17	16	ralrimiva	⊢ ( 𝑥 ∈ ( ℤ ∖ { 0 } ) → ∀ 𝑦 ∈ ℤ ( ( 𝑥 · 𝑦 ) = 0 → 𝑦 = 0 ) )
18		eqid	⊢ ( RLReg ‘ ℤring ) = ( RLReg ‘ ℤring )
19		zringbas	⊢ ℤ = ( Base ‘ ℤring )
20		zringmulr	⊢ · = ( .r ‘ ℤring )
21		zring0	⊢ 0 = ( 0g ‘ ℤring )
22	18 19 20 21	isrrg	⊢ ( 𝑥 ∈ ( RLReg ‘ ℤring ) ↔ ( 𝑥 ∈ ℤ ∧ ∀ 𝑦 ∈ ℤ ( ( 𝑥 · 𝑦 ) = 0 → 𝑦 = 0 ) ) )
23	3 17 22	sylanbrc	⊢ ( 𝑥 ∈ ( ℤ ∖ { 0 } ) → 𝑥 ∈ ( RLReg ‘ ℤring ) )
24	23	ssriv	⊢ ( ℤ ∖ { 0 } ) ⊆ ( RLReg ‘ ℤring )
25	19 18 21	isdomn2	⊢ ( ℤring ∈ Domn ↔ ( ℤring ∈ NzRing ∧ ( ℤ ∖ { 0 } ) ⊆ ( RLReg ‘ ℤring ) ) )
26	2 24 25	mpbir2an	⊢ ℤring ∈ Domn
27		isidom	⊢ ( ℤring ∈ IDomn ↔ ( ℤring ∈ CRing ∧ ℤring ∈ Domn ) )
28	1 26 27	mpbir2an	⊢ ℤring ∈ IDomn