1
$\begingroup$

How does on prove $\gcd(a, b) = 1 \wedge a\ |\ b\ c \Rightarrow a \ | \ c $ with as elementary steps as possible (i.e. not using the fundamental theorem of arithmetic (unique prime factorization))?

EDIT: I saw that this theorem is called Gauss Theorem and is proved formally for integers $\mathbb Z$ in Coq, https://coq.inria.fr/library/Coq.ZArith.Znumtheory.html#Gauss

EDIT: Clarification: I forgot to tell that I want to prove this for the natural numbers $\mathbb N \geq 0$. Is Bezout's lemma applicable for the natural numbers, or is some other method needed?

$\endgroup$
4
  • $\begingroup$ Yes it seem to be a dupe. Sorry about that. $\endgroup$
    – larsr
    Commented Nov 20, 2015 at 19:08
  • 1
    $\begingroup$ For a very elementary proof (only euclidean division), not mentioned in the above link, you can take a look at my answer to a similar question. $\endgroup$
    – Bernard
    Commented Nov 20, 2015 at 20:06
  • $\begingroup$ Thanks, I'll give it a try! I was hoping for a constructive proof - just saying that there exists a smallest element in the set with the desired properties is a bit messy (I'm trying to do a formal proof), but is doable I'm sure. $\endgroup$
    – larsr
    Commented Nov 20, 2015 at 22:02
  • 1
    $\begingroup$ The proof I gave (I think it's Cauchy's) relies precisely on the fact that $\mathbf N$ is well ordered. $\endgroup$
    – Bernard
    Commented Nov 20, 2015 at 22:25

1 Answer 1

0
$\begingroup$

I am not sure if Bezout's theorem is allowed or not. If $\gcd(a,b)=1$, then by Bezouts's theorem there exist $m,n \in \mathbb{Z}$ such that $ma+nb=1$. It follows that $mac+nbc=c$. Therefore since $a$ divides $mac$ and $nbc$ it must divide $c=mac+nbc$.

$\endgroup$
4
  • $\begingroup$ Actually I needed something more trivial (or a trivial proof of Bezouts' theorem). Just using "obvious" properties of gcd and divisibility... $\endgroup$
    – larsr
    Commented Nov 20, 2015 at 19:09
  • $\begingroup$ Is my proof here trivial enough: math.stackexchange.com/questions/1533795/bezouts-theorem/… $\endgroup$
    – Nex
    Commented Nov 20, 2015 at 19:29
  • $\begingroup$ Thanks! (see my comment above about a constructive proof...) $\endgroup$
    – larsr
    Commented Nov 20, 2015 at 22:03
  • $\begingroup$ A clarification: I'd like to do the proof for the natural numbers $0,1,2,...$. I don't think Bezout's lemma holds for the natural numbers, since one of the coefficients usually is negative. Or am I mistaken? $\endgroup$
    – larsr
    Commented Nov 20, 2015 at 23:35

Not the answer you're looking for? Browse other questions tagged .