Resolve does not resolve this statement with quantifier

I’m trying to use Resolve to get a condition on a parameter for which the statement is true, but it doesn’t look like it’s working:

Resolve[Exists[a, a > 0, Element[Sqrt[100 + a^4]/a, Rationals]], Rationals]

The statement does in fact have parameter values that make it true. For example, 3/2 or 20/3 are some instances of a that work. How can I have Mathematica solve this problem?



2 Answers


I do not know how to get Resolve to find your answers; however, Reduce can find solutions. Rewrite your equation with a=u/va=u/v, where uu and vv are coprime integers greater than zero. Hence, √u4+100∗v4/(u∗v)=c/d\sqrt{u^4+100*v^4}/(u*v)=c/d, where cc and dd are coprime integers greater than zero. If the square root returns an irrational, then there is no solution. If the square root returns an integer mm, then we have a solution.

Block[{r, u, v, m},
r = {ToRules[
Reduce[{m^2 == u^4 + 100*v^4, u>0, m>0, GCD[u,v]==1}, Integers]
If[r =!= {}, {u, v, m} /. r, {}],
{v, 1, 1000}],

The solutions come in pairs. If u/vu/v is a solution, then so is 10∗v/u10*v/u, both giving the same result c/dc/d. Up to v=5000v=5000 there are 4 solutions {u,v}\{u,v\} of {3,2}, {20,3}, {1519,492}, and {4920,1519}.

If using Reduce is a cheat, then consider writing m2−x2=100∗y2m^2-x^2=100*y^2, where x=u2x=u^2 and y=v2y=v^2. Assume y=1,4,9,…y=1,4,9,… is given, find the divisors pairs p∗q=100∗y2p*q=100*y^2, and {m,x}\{m,x\} via p=m−xp=m-x and q=m+xq=m+x. Save solutions with square xx.

Short answer is: I don’t believe you can make Mathematica solve this because math does not know how to solve this.

The longer version might not be 100% correct, since I am not a mathematician, but it goes somewhere along this:

The problem you’re trying to solve here boils down to the question of “Is a specific rational number a square of another rational number?”. And there is no constructive solution to this problem. The only known way to list all numbers that are squares of other numbers is to actually calculate them one by one from a list of all rationals.

So that’s what you can do with your problem. You can write an algorithm that will get you first 10, 100, 1000 or however much of rationals that solve it, but there still will be infinitely more of those to go, and there is no simpler way to get them all.



Thinks for your advices.
– yode
Jan 16 at 12:27