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 ⊢ ∥ = x y | x ∈ ℤ ∧ y ∈ ℤ ∧ ∃ n ∈ ℤ n ⁢ x = y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdvds class ∥
1 vx setvar x
2 vy setvar y
3 1 cv setvar x
4 cz class ℤ
5 3 4 wcel wff x ∈ ℤ
6 2 cv setvar y
7 6 4 wcel wff y ∈ ℤ
8 5 7 wa wff x ∈ ℤ ∧ y ∈ ℤ
9 vn setvar n
10 9 cv setvar n
11 cmul class ×
12 10 3 11 co class n ⁢ x
13 12 6 wceq wff n ⁢ x = y
14 13 9 4 wrex wff ∃ n ∈ ℤ n ⁢ x = y
15 8 14 wa wff x ∈ ℤ ∧ y ∈ ℤ ∧ ∃ n ∈ ℤ n ⁢ x = y
16 15 1 2 copab class x y | x ∈ ℤ ∧ y ∈ ℤ ∧ ∃ n ∈ ℤ n ⁢ x = y
17 0 16 wceq wff ∥ = x y | x ∈ ℤ ∧ y ∈ ℤ ∧ ∃ n ∈ ℤ n ⁢ x = y