zringidom

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

		Ref	Expression
	Assertion	zringidom	$⊢ ℤ_{ring} \in IDomn$

Proof

Step	Hyp	Ref	Expression
1		zringcrng	$⊢ ℤ_{ring} \in CRing$
2		zringnzr	$⊢ ℤ_{ring} \in NzRing$
3		eldifi	$⊢ x \in (ℤ ∖ \{0\}) \to x \in ℤ$
4	3	ad2antrr	$⊢ ((x \in (ℤ ∖ \{0\}) \land y \in ℤ) \land x y = 0) \to x \in ℤ$
5	4	zcnd	$⊢ ((x \in (ℤ ∖ \{0\}) \land y \in ℤ) \land x y = 0) \to x \in ℂ$
6		simplr	$⊢ ((x \in (ℤ ∖ \{0\}) \land y \in ℤ) \land x y = 0) \to y \in ℤ$
7	6	zcnd	$⊢ ((x \in (ℤ ∖ \{0\}) \land y \in ℤ) \land x y = 0) \to y \in ℂ$
8		simpr	$⊢ ((x \in (ℤ ∖ \{0\}) \land y \in ℤ) \land x y = 0) \to x y = 0$
9		mul0or	$⊢ (x \in ℂ \land y \in ℂ) \to (x y = 0 \leftrightarrow (x = 0 \lor y = 0))$
10	9	biimpa	$⊢ ((x \in ℂ \land y \in ℂ) \land x y = 0) \to (x = 0 \lor y = 0)$
11	5 7 8 10	syl21anc	$⊢ ((x \in (ℤ ∖ \{0\}) \land y \in ℤ) \land x y = 0) \to (x = 0 \lor y = 0)$
12		eldifsni	$⊢ x \in (ℤ ∖ \{0\}) \to x \neq 0$
13	12	ad2antrr	$⊢ ((x \in (ℤ ∖ \{0\}) \land y \in ℤ) \land x y = 0) \to x \neq 0$
14	13	neneqd	$⊢ ((x \in (ℤ ∖ \{0\}) \land y \in ℤ) \land x y = 0) \to \neg x = 0$
15	11 14	orcnd	$⊢ ((x \in (ℤ ∖ \{0\}) \land y \in ℤ) \land x y = 0) \to y = 0$
16	15	ex	$⊢ (x \in (ℤ ∖ \{0\}) \land y \in ℤ) \to (x y = 0 \to y = 0)$
17	16	ralrimiva	$⊢ x \in (ℤ ∖ \{0\}) \to \forall y \in ℤ (x y = 0 \to y = 0)$
18		eqid	$⊢ RLReg (ℤ_{ring}) = RLReg (ℤ_{ring})$
19		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
20		zringmulr	$⊢ \times = \cdot_{ℤ_{ring}}$
21		zring0	$⊢ 0 = 0_{ℤ_{ring}}$
22	18 19 20 21	isrrg	$⊢ x \in RLReg (ℤ_{ring}) \leftrightarrow (x \in ℤ \land \forall y \in ℤ (x y = 0 \to y = 0))$
23	3 17 22	sylanbrc	$⊢ x \in (ℤ ∖ \{0\}) \to x \in RLReg (ℤ_{ring})$
24	23	ssriv	$⊢ ℤ ∖ \{0\} \subseteq RLReg (ℤ_{ring})$
25	19 18 21	isdomn2	$⊢ ℤ_{ring} \in Domn \leftrightarrow (ℤ_{ring} \in NzRing \land ℤ ∖ \{0\} \subseteq RLReg (ℤ_{ring}))$
26	2 24 25	mpbir2an	$⊢ ℤ_{ring} \in Domn$
27		isidom	$⊢ ℤ_{ring} \in IDomn \leftrightarrow (ℤ_{ring} \in CRing \land ℤ_{ring} \in Domn)$
28	1 26 27	mpbir2an	$⊢ ℤ_{ring} \in IDomn$

Metamath Proof Explorer

Theorem zringidom

Proof