Definition df-dvds

Description: Define the divides relation, see definition in ApostolNT p. 14. (Contributed by Paul Chapman, 21-Mar-2011)

	Ref	Expression
Assertion	df-dvds	⊢ ∥ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ∃ 𝑛 ∈ ℤ ( 𝑛 · 𝑥 ) = 𝑦 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdvds	⊢ ∥
1		vx	⊢ 𝑥
2		vy	⊢ 𝑦
3	1	cv	⊢ 𝑥
4		cz	⊢ ℤ
5	3 4	wcel	⊢ 𝑥 ∈ ℤ
6	2	cv	⊢ 𝑦
7	6 4	wcel	⊢ 𝑦 ∈ ℤ
8	5 7	wa	⊢ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ )
9		vn	⊢ 𝑛
10	9	cv	⊢ 𝑛
11		cmul	⊢ ·
12	10 3 11	co	⊢ ( 𝑛 · 𝑥 )
13	12 6	wceq	⊢ ( 𝑛 · 𝑥 ) = 𝑦
14	13 9 4	wrex	⊢ ∃ 𝑛 ∈ ℤ ( 𝑛 · 𝑥 ) = 𝑦
15	8 14	wa	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ∃ 𝑛 ∈ ℤ ( 𝑛 · 𝑥 ) = 𝑦 )
16	15 1 2	copab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ∃ 𝑛 ∈ ℤ ( 𝑛 · 𝑥 ) = 𝑦 ) }
17	0 16	wceq	⊢ ∥ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ∃ 𝑛 ∈ ℤ ( 𝑛 · 𝑥 ) = 𝑦 ) }