A proof system for GCD?

As is well known, if $x,y$ are natural numbers then their GCD $(x,y)$ has a representation $(x,y) = ax + by$ where $a,b$ are natural. Now let's prove that if $(x,y)=1$ then $(xy,x+y) = 1$. Starting from $ax+by=1$, $$1 = (ax+by)^2 = a^2x^2 + b^2y^2 + 2abxy = (a^2x+b^2y)(x+y) - (a-b)^2xy.$$ The reverse implication is trivial in this method. The proof can be generalized to show that if $(x,y,z)=1$ then $(xyz,xy+xz+yz,x+y+z)=1$ and vice versa.

Can this idea be molded into a reasonably strong formal proof system for some fragment of number theory?

We're competing with divisibility proofs, which we'd like to forbid somehow. For example, the original statement can be proven as follows. Suppose $p$ is a prime dividing $(xy,x+y)$. Since $p|xy$ and $p$ is prime, either $p|x$ or $p|y$. From $p|x+y$ we get that $p|(x,y)$.

-

$\rm\quad\quad (x,y) \ \supset\ (xy,\ x+y)\ \supset\ (x,y)^2\ \$ therefore $\rm\ \ (xy,\ x+y)\ =\ 1\ \iff\ (x,y)\ =\ 1$
Notice how employing ideals has eliminated obfuscatory information such as the extraneous coefficients $\ a,\:b\$ in the original proof. That done, the innate structure becomes much clearer.