theorem Th73: :: POLYNOM9:73

for M being Jpolynom of 4, F_Complex
for x1, x2, x3 being Nat st x1 is odd & x2 is odd holds
for z being Integer st eval ((Jsqrt M),(@ <%z,x1,(4 * x2),(16 * x3)%>)) = 0 holds
( x1 is square & x2 is square & x3 is square & - z <= ((sqrt x1) + (2 * (sqrt x2))) + (4 * (sqrt x3)) )