# Is there an automated way to prove really boring elementary number theoretic results?

Motivation: I'm writing a proof, and within it, I need to prove:

Conjecture: Let $p$ be an odd prime (i.e. $p \neq 2$). Let $c \geq 2$, $d \geq 1$ and $r \geq 1$. If $p^r$ divides $cd$, then $d(c-1) \geq r+1$.

This conjecture, should it prove to be true (and I suspect it will [it seems to be like "prove elephants are bigger than mosquitos"], unless I've missed a few small cases), would be a rather uninteresting result and no real insight into the problem I'm studying. This leads me to the question:

Question: Does there exist a software package that would allow me to automatically prove (or disprove) this conjecture (or results like this)?

-
You've missed the small case $p=2, c=2, d=1, r=1$. – Chris Eagle Mar 10 '11 at 3:24
By the solution of one of Hilbert's problems, there is no automated way to solve number theoretic results in general. How do you recognize the boring ones among them? – Mariano Suárez-Alvarez Mar 10 '11 at 3:29
@Mariano: You stare at them for one minute. If you yawn, it's a boring theorem. – Arturo Magidin Mar 10 '11 at 3:34
$x^n + y^n = z^n$ has no solutions in positive integers with $n > 2$. I have a truly remarkable proof of this fact but the comment box is too small to contain it. – Michael Lugo Mar 10 '11 at 4:07
@Alex oh, I'm not claiming it's new. But you really don't want me coming up with my own jokes. – Michael Lugo Mar 10 '11 at 4:30