Description: Define the divides relation, see definition in ApostolNT p. 14. (Contributed by Paul Chapman, 21-Mar-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | df-dvds | ⊢ ∥ = { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ∃ 𝑛 ∈ ℤ ( 𝑛 · 𝑥 ) = 𝑦 ) } |
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 | ⊢ ∥ = { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ∃ 𝑛 ∈ ℤ ( 𝑛 · 𝑥 ) = 𝑦 ) } |