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	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → 𝑥 ∈ ℤ )
2	1	anim1i	⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ∃ 𝑧 ∈ ℤ ( 𝑧 · 𝑥 ) = 𝑦 ) → ( 𝑥 ∈ ℤ ∧ ∃ 𝑧 ∈ ℤ ( 𝑧 · 𝑥 ) = 𝑦 ) )
3		simpl	⊢ ( ( 𝑥 ∈ ℤ ∧ ∃ 𝑧 ∈ ℤ ( 𝑧 · 𝑥 ) = 𝑦 ) → 𝑥 ∈ ℤ )
4		zmulcl	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( 𝑧 · 𝑥 ) ∈ ℤ )
5	4	ancoms	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) → ( 𝑧 · 𝑥 ) ∈ ℤ )
6		eleq1	⊢ ( ( 𝑧 · 𝑥 ) = 𝑦 → ( ( 𝑧 · 𝑥 ) ∈ ℤ ↔ 𝑦 ∈ ℤ ) )
7	5 6	syl5ibcom	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) → ( ( 𝑧 · 𝑥 ) = 𝑦 → 𝑦 ∈ ℤ ) )
8	7	rexlimdva	⊢ ( 𝑥 ∈ ℤ → ( ∃ 𝑧 ∈ ℤ ( 𝑧 · 𝑥 ) = 𝑦 → 𝑦 ∈ ℤ ) )
9	8	imp	⊢ ( ( 𝑥 ∈ ℤ ∧ ∃ 𝑧 ∈ ℤ ( 𝑧 · 𝑥 ) = 𝑦 ) → 𝑦 ∈ ℤ )
10		simpr	⊢ ( ( 𝑥 ∈ ℤ ∧ ∃ 𝑧 ∈ ℤ ( 𝑧 · 𝑥 ) = 𝑦 ) → ∃ 𝑧 ∈ ℤ ( 𝑧 · 𝑥 ) = 𝑦 )
11	3 9 10	jca31	⊢ ( ( 𝑥 ∈ ℤ ∧ ∃ 𝑧 ∈ ℤ ( 𝑧 · 𝑥 ) = 𝑦 ) → ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ∃ 𝑧 ∈ ℤ ( 𝑧 · 𝑥 ) = 𝑦 ) )
12	2 11	impbii	⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ∃ 𝑧 ∈ ℤ ( 𝑧 · 𝑥 ) = 𝑦 ) ↔ ( 𝑥 ∈ ℤ ∧ ∃ 𝑧 ∈ ℤ ( 𝑧 · 𝑥 ) = 𝑦 ) )
13	12	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ∃ 𝑧 ∈ ℤ ( 𝑧 · 𝑥 ) = 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℤ ∧ ∃ 𝑧 ∈ ℤ ( 𝑧 · 𝑥 ) = 𝑦 ) }
14		df-dvds	⊢ ∥ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ∃ 𝑧 ∈ ℤ ( 𝑧 · 𝑥 ) = 𝑦 ) }
15		zringbas	⊢ ℤ = ( Base ‘ ℤring )
16		eqid	⊢ ( ∥r ‘ ℤring ) = ( ∥r ‘ ℤring )
17		zringmulr	⊢ · = ( .r ‘ ℤring )
18	15 16 17	dvdsrval	⊢ ( ∥r ‘ ℤring ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℤ ∧ ∃ 𝑧 ∈ ℤ ( 𝑧 · 𝑥 ) = 𝑦 ) }
19	13 14 18	3eqtr4i	⊢ ∥ = ( ∥r ‘ ℤring )