I think I'm missing something... isn't there an error in the proof when applying the theorem of the principle of infinite descent?

The theorem requires proving the following premise/antecedent (to deduce the consequent):

  ∀x ∈ X. Φ(x) ⟹ ∃y ∈ X.  y ⊏ x  ∧  (...)

... but I don't see how this can be proved when x=0. By substituting `x` for `0` (and using Z as the set X and |<| as the well-founded relation) you get:

  Φ(0) ⟹ ∃y ∈ Z. y |<| 0

Unfolding Φ:

  (∃b ∈ Z. 0^2 = 2 b^2) ⟹ ∃y ∈ Z. y |<| 0

The antecedent of this implication is true (when b = 0), so now you have to prove:

  ∃y ∈ Z. y |<| 0

However, this can't be proved because no `y` satisfies the |<| well-founded relation when applied to zero.

Therefore, this article's sentence doesn't seem to be true:

> Having satisfied the premises of the principle, we use it to deduce that no `a` satisfies the property

... which in fact cannot be true, because `a=0` does satisfy the property `∃b ∈ Z. a^2 = 2 b^2`, does it not? Consider `b=0`.

So what am I missing?

Edit: in fact, if the theorem could be applied in this case, then the conclusion of the theorem would be:

  ∀x ∈ Z. ¬(∃b ∈ Z. x^2 = 2 b^2)

Which is equivalent to:

  ∀x ∀y ∈ Z. ¬(x^2 = 2 y^2)

... which is clearly false when x=0 and y=0. So it seems like the theorem of infinite descent cannot be used to reach this conclusion. Some kind of false assumption would have to exist, but no false assumption was used to instantiate this theorem.