To finish a proof, I need to solve a system of two polynomials with integer coefficients in two variables, $\{F_1(x,y)=0,\,F_2(x,y)=0\}$, and then show that no solutions satisfy $0<x<1$ and $y>0$, where $F_1,F_2$ are as follows:
$$ \begin{equation*} \begin{split} F_1(x,y) &= -168 x^{11} - 1386 x^{10} y + x^9 (730 - 420 y^2) - 9 x^8 y (-489 + 370 y^2) + 14 x^6 y (-135 + 256 y^2 + 6 y^4) \\ &+ 6 x^2 y^5 (747 - 282 y^2 + 29 y^4) - 8 x^3 y^4 (513 + 209 y^2 + 39 y^4) - 16 x^7 (45 - 26 y^2 + 72 y^4) + y^7 (270 + 79 y^2 + 78 y^4) \\ &+ 30 x^4 y^3 (-249 - 38 y^2 + 138 y^4) - 2 x y^6 (-1134 + 67 y^2 + 186 y^4) - 12 x^5 y^2 (171 - 363 y^2 + 298 y^4)\\ &\\ F_2(x,y) &= -126 x^{11} - 84 x^{10} y + x^9 (489 - 1110 y^2) - 8 x^8 y (-13 + 72 y^2) + 12 y^7 (216 - 65 y^2 + 4 y^4) \\ &+ 6 x^7 (-45 + 256 y^2 + 10 y^4) - 12 x^4 y^3 (342 + 209 y^2 + 52 y^4) + 6 x^3 y^4 (1245 - 658 y^2 + 87 y^4) \\ &+ 3 x y^6 (630 + 237 y^2 + 286 y^4) - 12 x^6 y (57 - 242 y^2 + 298 y^4) - 4 x^2 y^5 (-1701 + 134 y^2 + 465 y^4) \\ &+ 6 x^5 y^2 (-747 - 190 y^2 + 966 y^4) \end{split} \end{equation*}$$
I've used Mathematica to compute the solutions and find that my claim is true. I understand that Mathematica's algorithm to solve these systems is based on Grobner basis but unfortunately I lack the background necessary to understand them well. My questions are:
- Can I trust that Mathematica correctly finds all the real solutions to the system?
- If so, what theoretical results ensure that all the solutions to the system can be computed via these algorithms?
Thanks very much for your help!