Complete proof that sum of rationals is rational

Hi, I did a search, admittedly brief, trying to find a complete proof that the sum of two rational numbers is a rational number. I have a proof in my discrete mathematics book. When it comes to proving useful stuff, the proofs in the book change from showing each step to being much more informal. The reason given that showing each step would be tedious. Which is fair enough. But for fun's sake, how would such a proof go?

The abbreviated proof is:

Prove that the sum of two rational numbers is rational.

Direct proof:

Suppose that s and r are rational numbers.

From the definition of a rational number, it follows that there are integers p and q, with q != 0, such that r = p / q, and integers t and u, with u != 0, such that s = t / u.

Thus, r + s = p / q + t / u = (pu + qt) / qu.

Because q and u are != 0 and integers it follows that qu is != 0 and an integer. We have expressed r + s as a ratio of two integers. This means r + s is rational.

To put this into quantifier logic.

Prove that for each real number r and real number s, if r and s are rational numbers, then r + s is rational.

Prove: VrVs(R(r) ^ R(r) -> R(r + s))

1. Vx(R(x) -> EyEz(x = y / z ^ z != 0)) (definition of rational x is rational, y and z are integers)

2. R(r) (hypothesis r is rational)

3. R(s) (hypothesis s is rational)

4. R(r) -> r = p / q ^ q != 0 (universal instantiation of 1)

5. R(s) -> s = t / u ^ u != 0 (universal instantiation of 1)

6. r = p / q ^ q != 0 (modus ponens 2,4)

7. s = t / u ^ u != 0 (modus ponens 3,5)

8. p / q (simplification 6)

9. t / u (simplification 7)

10. r + s = p / q + t / u

11. r + s = (pu + qt) / qu

12.....

That's about as far as I've got. Some of the steps abov like 10 and 11 just seem like math, not a logical proof. How would this proof go is proper quantifier logic with (or without) equality?

Thanks in advance.

Legend:

Vx = for each x (universal quantifier)

Ex = there is (existential quantifier)

R(x) = x is rational

^ = and

-> = if/then

!= is not equal to