Metamath Proof Explorer


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 ∥ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ∃ 𝑛 ∈ ℤ ( 𝑛 · 𝑥 ) = 𝑦 ) }