Proving ∀x (0|x ↔ x = 0) (divisor by Zero) - Euclidean Algorithm

Question

I am trying to proof the total correction of Euclidean Algorithm, so I am up to proof one of the following properties which is divisor by Zero.

Given this Axiom:

(div) ∀x∀y (x | y ↔ ∃n y = n • x)

I want to proof:

(divby0) ∀x (0|x ↔ x = 0)

---

My attempt so far: Using the one of the properties of multiplication which is

(MULT0a) ∀x 0 ⋅ x = 0

and the Natural deduction rules

Steps:

1. (div) ∀x∀y (x | y ↔ ∃n y = n • x)
2. (MULT0a) ∀x 0 ⋅ x = 0

3. ∀y (0 | y ↔ ∃n y = n • 0)      -- ∀-elim 1

4. (0 | a ↔ ∃n a = n • 0)          -- ∀-elim 3, let a->Natural numbers

5. (∃n a = n • 0 → 0 | a)          -- ↔ elim2, 4 

6. 0 . a = 0                       -- ∀elim,2 

7. 

8. 

How could I fix it or improve it?

Answer 1

For one "side", we must start assuming :

$x = 0$

then deriving, by use of transitivity of $=$ and axiom $0 = a \times 0$ that :

$x = n \times 0$

and from this, by $\exists$-intro :

$\exists n (x = n \times 0)$, that is : $0|x$.

For the other "side", from $0|x$, i.e. $\exists n (x = n \times 0)$, assume for $\exists$-elim $n$ such that $x = n \times 0$.

From the axiom $n \times 0 = 0$ transitivity of $=$ we derive :

$x = 0$;

thus, by $\exists$-elim (becuase $n$ is not free in $x = 0$) we conclude :

$x = 0$.

In conclusion, we have proved that :

$x = 0 \vdash \exists n (x = n \times 0)$,

and that :

$\exists n (x = n \times 0) \vdash x = 0$,

i.e. by $\leftrightarrow$-intro :

$\vdash x = 0 \leftrightarrow 0|x$.

One last step of $\forall$-intro and we have :

$\vdash \forall x (x = 0 \leftrightarrow 0|x)$.