This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → 𝑥 ∈ ℤ )
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 )