Metamath Proof Explorer

Theorem dvdsrzring

Description: Ring divisibility in the ring of integers corresponds to ordinary divisibility in ZZ . (Contributed by Stefan O'Rear, 3-Jan-2015) (Revised by AV, 9-Jun-2019)

		Ref	Expression
	Assertion	dvdsrzring	$⊢ ∥ = ∥_{r} (ℤ_{ring})$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (x \in ℤ \land y \in ℤ) \to x \in ℤ$
2	1	anim1i	$⊢ ((x \in ℤ \land y \in ℤ) \land \exists z \in ℤ z x = y) \to (x \in ℤ \land \exists z \in ℤ z x = y)$
3		simpl	$⊢ (x \in ℤ \land \exists z \in ℤ z x = y) \to x \in ℤ$
4		zmulcl	$⊢ (z \in ℤ \land x \in ℤ) \to z x \in ℤ$
5	4	ancoms	$⊢ (x \in ℤ \land z \in ℤ) \to z x \in ℤ$
6		eleq1	$⊢ z x = y \to (z x \in ℤ \leftrightarrow y \in ℤ)$
7	5 6	syl5ibcom	$⊢ (x \in ℤ \land z \in ℤ) \to (z x = y \to y \in ℤ)$
8	7	rexlimdva	$⊢ x \in ℤ \to (\exists z \in ℤ z x = y \to y \in ℤ)$
9	8	imp	$⊢ (x \in ℤ \land \exists z \in ℤ z x = y) \to y \in ℤ$
10		simpr	$⊢ (x \in ℤ \land \exists z \in ℤ z x = y) \to \exists z \in ℤ z x = y$
11	3 9 10	jca31	$⊢ (x \in ℤ \land \exists z \in ℤ z x = y) \to ((x \in ℤ \land y \in ℤ) \land \exists z \in ℤ z x = y)$
12	2 11	impbii	$⊢ ((x \in ℤ \land y \in ℤ) \land \exists z \in ℤ z x = y) \leftrightarrow (x \in ℤ \land \exists z \in ℤ z x = y)$
13	12	opabbii	$⊢ \{⟨x, y⟩ \| ((x \in ℤ \land y \in ℤ) \land \exists z \in ℤ z x = y)\} = \{⟨x, y⟩ \| (x \in ℤ \land \exists z \in ℤ z x = y)\}$
14		df-dvds	$⊢ ∥ = \{⟨x, y⟩ \| ((x \in ℤ \land y \in ℤ) \land \exists z \in ℤ z x = y)\}$
15		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
16		eqid	$⊢ ∥_{r} (ℤ_{ring}) = ∥_{r} (ℤ_{ring})$
17		zringmulr	$⊢ \times = \cdot_{ℤ_{ring}}$
18	15 16 17	dvdsrval	$⊢ ∥_{r} (ℤ_{ring}) = \{⟨x, y⟩ \| (x \in ℤ \land \exists z \in ℤ z x = y)\}$
19	13 14 18	3eqtr4i	$⊢ ∥ = ∥_{r} (ℤ_{ring})$