Proving and disproving First Order Logic statements in $\mathbb{N}$.

Question

Working on the book: Daniel J. Velleman. "HOW TO PROVE IT: A Structured Approach, Second Edition" (p. 77)

7. Are these statements true or false? The universe of discourse is $\mathbb{N}$.

(c) $\forall x\exists y(x - 2y = 0)$.

(d) $\forall x(x < 10 \to \forall y(y < x \to y < 9))$.

Disproof of (c):

I need to show the negation of $\forall x\exists y(x < 10 \to \forall y(y < x \to y < 9))$ is true.

• $\lnot(\textsf{1 is even})$
  • Assume $1 - 2b = 0$
    • 1 = 2b
    • 1 is even
    • $\lnot$(1 is even)
    • $\bot$
  • $1 - 2b \neq 0$
  • $\forall y(1 - 2y \neq 0)$, $\quad\to \forall\textsf{ Introduction}$
  • $\exists x\forall y(x - 2y \neq 0)$, $\quad\to \exists\textsf{ Introduction}$

Proof of (d):

• Assume $a < 10$, $\quad a \in \mathbb{N}$
  • Assume b < a, $\quad b \in \mathbb{N}$
    • b < 10, by transitivity of $<$
    • $\vdots$
    • $b < 9$
  • $b < a \to b < 9$, $\quad\to \textsf{Introduction}$
  • $\forall y(y < a \to y < 9)$, $\quad\to \forall\textsf{ Introduction}$
• $a < 10 \to \forall y(y < a \to y < 9)$
• $\forall x(x < 10 \to \forall y(y < x \to y < 9)$, $\quad\to \forall\textsf{ Introduction}$

Questions:

Are the proof skeleton of c and disproof of d correct ? How can I fill the gaps in point c ?

EDIT: taking inspiration in Daniel Schepler's comment, I revised point (d).

Proof of (d):

• Assume $a < 10$, $\quad a \in \mathbb{N}$
  • Assume $b < a$, $\quad b \in \mathbb{N}$
    • $a<9+1$
    • $a<9+1 \to a <= 9$
    • $a<=9$
    • $b<a \land a<=9$
    • $b < a \land a <= 9 \to b < 9$
    • $b < 9$
  • $b < a \to b < 9$, $\quad\to \textsf{Introduction}$
  • $\forall y(y < a \to y < 9)$, $\quad\to \forall\textsf{ Introduction}$
• $a < 10 \to \forall y(y < a \to y < 9)$
• $\forall x(x < 10 \to \forall y(y < x \to y < 9)$, $\quad\to \forall\textsf{ Introduction}$