Theorem dvdszrcl

Description: Reverse closure for the divisibility relation. (Contributed by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Assertion	dvdszrcl	⊢ ( 𝑋 ∥ 𝑌 → ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) )

Proof

Step	Hyp	Ref	Expression
1		df-dvds	⊢ ∥ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ∃ 𝑧 ∈ ℤ ( 𝑧 · 𝑥 ) = 𝑦 ) }
2		opabssxp	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ∃ 𝑧 ∈ ℤ ( 𝑧 · 𝑥 ) = 𝑦 ) } ⊆ ( ℤ × ℤ )
3	1 2	eqsstri	⊢ ∥ ⊆ ( ℤ × ℤ )
4	3	brel	⊢ ( 𝑋 ∥ 𝑌 → ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) )