I am looking for a proof of Euclid's Lemma, i.e if a prime number divides a product of two numbers then it must at least divide one of them.

I am coding this proof in Coq, and i'm doing it over natural numbers. I aim to prove the uniqueness of prime factorization (So I cannot use this lemma!). However, I can use the existence of a prime factorization, which I already proved.

I do not want to use the gcd algorithm as that would involve coding it in Coq and proving it is correct which may be difficult. The idea is to use this proof in a computer science course, so I do not want to overcomplicate things.

Is there any proof of this lemma that does not use gcd, or Bezout's lemma, or the uniqueness of prime factorization? Maybe something using induction?

Thank you in advance.

EDIT: The Proof should be on NATURAL NUMBERS. No answer did the proof in N.

  • $\begingroup$ Didn't you ask this very question a few hours ago? You got some answers, but they were by contradiction. However now that I know you are trying to do it in Coq, I would most recommend using gcd after all. It is not a very difficult algorithm at all. You can prove it correct using some simple facts about division with remainder, which you will need to prove in any case. $\endgroup$ – Jorik Dec 18 '15 at 21:11
  • $\begingroup$ @Jorik and I would also have to prove Bezout's lemma... Is ir easy? $\endgroup$ – Martin Copes Dec 18 '15 at 21:22
  • $\begingroup$ Beloit's lemma is easy. But please use gcd. $\endgroup$ – Dietrich Burde Dec 18 '15 at 21:34
  • $\begingroup$ @MartinCopes It won't be trivial of course. But the algorithm it self is not so complicated. The main benefit is that it will be constructive, which you kinda need since you're working in Coq. $\endgroup$ – Jorik Dec 18 '15 at 22:17
  • $\begingroup$ @Jorik However, I am also working with natural numbers.. Bezout's lemma is for Z. $\endgroup$ – Martin Copes Dec 18 '15 at 22:21

Claim 2 below should answer the question.

Since the only unit in $\mathbb{N}$ is $1$, we have

$p$ is prime iff $p\mid ab\implies p\mid a\lor p\mid b$

$p$ is irreducible iff $a\mid p\implies a=1\lor a=p$

Claim 1: $p$ is prime $\implies$ $p$ is irreducible

Proof: Assume that $a\mid p$. For some $b$, we have $$ p=ab\tag{1} $$ Since $p\mid ab$, we know that $p\mid a$ or $p\mid b$.

Case $p\mid a$: for some $c$, we have $a=pc$. Therefore, $(1)$ implies that $abc=a$. Since the only unit in $\mathbb{N}$ is $1$, we have that $b=c=1$. Therefore $a=p$.

Case $p\mid b$: for some $c$, we have $b=pc$. Therefore, $(1)$ implies that $abc = b$. Since the only unit in $\mathbb{N}$ is $1$, we have that $a=c=1$. Therefore, $a=1$.

Thus, assuming that $p$ is prime and $a\mid p$, we have shown that $a=1$ or $a=p$.


Claim 2: $p$ is irreducible $\implies$ $p$ is prime

Proof: Assume that $p$ is irreducible, $p\mid ab$, and $p\nmid a$. Let $g$ be the smallest positive element of the set $$ S=\{\,ax+py:x,y\in\mathbb{Z}\,\}\tag{2} $$ If $g\nmid p$, then there is an $r$ so that $0\lt r\lt g$ and $qg+r=p$. However, then $$ r=p-q(ax+py)=a(-qx)+p(1-qy)\in S\tag{3} $$ but $g$ is the smallest positive element of $S$. Therefore, $g\mid p$. Similarly, $g\mid a$.

Since $p$ is irreducible, $g=1$ or $g=p$. Since $p\nmid a$ and $g\mid a$, we must have $g=1$. Therefore, we have $x,y$ so that $$ 1=ax+py\tag{4} $$ Since $p\mid ab$, for some $c$, we have $ab=pc$. Multiply $(4)$ by $b$ to get $$ \begin{align} b &=abx+pby\\ &=p(cx+by)\tag{5} \end{align} $$ Equation $(5)$ says that $p\mid b$.

Thus, assuming that $p$ is irreducible and $p\mid ab$, we have shown that if $p\nmid a$, then $p\mid b$.


  • $\begingroup$ I know nothing about Coq. I don't know if my answer, although it shows what was asked, relates to what the OP needs. $\endgroup$ – robjohn Dec 18 '15 at 22:44
  • $\begingroup$ Thank you very much for your answer! It is almost what I needed to prove this lemma in Coq. However, there is one argument that seems difficult to formalize in Coq. It is the part of claim 2 where you prove that $g$ must divide $p$ and $a$. This whole argument with taking the smallest possible element of a set is not what I am looking for. Do you know any alternative proof for this Lemma? That is, the part where you state that $g$ and $a$ divide $p$. $\endgroup$ – Martin Copes Dec 19 '15 at 17:51
  • $\begingroup$ @MartinCopes: I am sorry, but I can't think of another approach that doesn't use something that uses Euclid's Lemma (making a circular argument). $\endgroup$ – robjohn Dec 19 '15 at 18:02
  • $\begingroup$ the problem with this proof is that it does not work with natural numbers. You are using Bézout's identity. You state that there exist some x and y in Z, such that 1 = ax + py.. but this identity does not hold for x and y in N. What I need is an argument that only uses natural numbers. Is this impossible? $\endgroup$ – Martin Copes Dec 19 '15 at 19:00
  • $\begingroup$ Maybe we could prove that: For all natural numbers $m$ $n$, if $m$ and $n$ are coprime then there exists $a$ and $b$ in N such that $am = bn + 1$. That would be enough to prove what we need here... $\endgroup$ – Martin Copes Dec 19 '15 at 19:12

The OP's stated goal is to prove the uniqueness of prime factorization using elementary/foundational techniques, perhaps by proving Euclid's lemma in a different way.

Since the end goal is to prove uniqueness in the FTA, of interest here are two similar elementary proofs.

(1) The wikipedia article: Elementary proof of uniqueness

which uses the distributivity law a couple of times.

(2) Bill Dubuque's: Elementary proof of the FTA

The 'hook' used there: every $n \gt 1$ has a least (unique) factor $p \ne 1$. The argument works around that to get the FTA.

I think that the techniques found in the above arguments are beautiful, although those who have not invested the time most likely would not agree.

In conclusion, a budding $\text{AI MATH BOT}$ might enjoy chewing on this elementary theory!

  • 1
    $\begingroup$ You can find a variant of Zermelo's direct proof of unique factroization in this answer, as well as another direct proof in another answer there. $\endgroup$ – Bill Dubuque May 21 '19 at 17:48

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.