theorem Th74: :: POLYNOM9:74

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