Como es bien sabido, si $x,y$ son números naturales, entonces, su MCD $(x,y)$ tiene una representación $(x,y) = ax + by$ donde $a,b$ son naturales. Ahora vamos a probar que si $(x,y)=1$$(xy,x+y) = 1$. A partir de $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$, y viceversa.
Puede que esta idea de ser moldeada en una razonablemente fuerte prueba formal del sistema para algún fragmento de la teoría de los números?
Estamos compitiendo con la divisibilidad de las pruebas, la que nos gustaría prohibir de alguna manera. Por ejemplo, el original de la declaración no puede ser probado de la siguiente manera. Supongamos $p$ es un primer dividiendo $(xy,x+y)$. Desde $p|xy$ $p$ es primo, $p|x$ o $p|y$. De $p|x+y$ tenemos que $p|(x,y)$.
