So in trying to formulate this proof, based on the statement that:
$gcd(m, n): ∀m, n, a ∈ \mathbb Z,∃ e \in \mathbb N, ((e|m ∧ e|n) ∧ (∀ d ∈ \mathbb N, d|n ∧ d|m \Rightarrow d\leq e))$
I've attempted to translate the following statement into predicate logic and I've been on the fence in terms of what translation is actually correct: $gcd(m, n) = gcd(n, m-an)$.
What I have now is:
$∀m, n, a ∈ \mathbb Z, ∃ e ∈ \mathbb N,((e|m ∧ e|n) ∧(∀ d ∈ N, d|n ∧ d|m => d≤e)) $
$∧ ∃ f ∈ \mathbb N, (f|n ∧ f|(m−an)) ∧ (∀ d ∈ \mathbb N, d|n ∧ d|m−an) \Rightarrow d ≤ f) \Rightarrow (f=e))$
There are 2 assumptions that I'm allowed to use:
1) $∀a,b,c ∈ \mathbb N, a|b ∧ b|c ⇒ a|c$
2) $∀a,b,d∈\mathbb Z, d|a ∧ d|b \Rightarrow ∀p, q ∈ \mathbb Z, d|(pa+qb)$
There are a few things that I've tried, but it feels like the proofs I've been able to formulate are lacking. Is my initial translation incorrect? Can anyone point me in the right direction?
Call $\ d=\mathrm{gcd}(m,n)$. Then $d\vert m$ and $d\vert n$, this implies that $$ d\vert m-an$$ for all $a\in\mathbb{Z}$. So, $d$ satisfies $$ d\vert n\ \ \text{and} \ \ d\vert (m-an)$$ this means that $d$ is a common divisor of $n$ and $m-an$. Suppose that $x$ is also a common divisor of $n$ and $m-an$. Thus, $x\vert n$ implies $x\vert an$. So, $x\vert an$ and $x\vert m-an$. Hence $x\vert(an+(m-an))=m$. Finally, as $d=\mathrm{gcd}(m,n)$ we have: $$x\vert m \ \text{and}\ \ x\vert n\ \Longrightarrow\ x\vert d$$