Attempt to prove the $∀d∀x∀y (d | x ∧ d | y ∧ x ≤ y → d | y- x)$ property of the “divides” relation for non-negative integers

Question

I am attempting to prove the $∀d∀x∀y (d | x ∧ d | y ∧ x ≤ y → d | y- x)$ property of the “divides” relation for non-negative integers, but am having a little difficulty and am hoping someone can help.

I have access to the standard rules of natural deduction, the following axioms:

and the following useful formulas:

---

Here is my attempt so far:

Answer 1

The key formula you will have to use is:

$\forall x \forall y \forall z (z \not = 0 \rightarrow (x\cdot z \le y\cdot z \rightarrow x \le y))$

So, you will need to first consider the special case where $a=0$, but in that case you can easily show that it must be the case that $a1=0$ and $a2=0$, and it is also easy to show that $0|0-0$ so you're done.

So then you can consider $a \not = 0$, and s0 you have:

1. $a \not = 0$

2. $a|a1$

3. $a|a2$

4. $a1 \le a2$

5. $a1 = a3\cdot a$

6. $a2 = a4\cdot a$

So then using some = Elim's:

6. $a3\cdot a \le a4 \cdot a$

And now you use the key formula to get:

7. $a3\cdot a \le a4 \cdot a \rightarrow a3 \le a4$

8. $a3 \le a4$ (6,7)

and you already have the rest.