theorem Th77: :: POLYNOM9:77

ex K3 being INT -valued Polynomial of 8,F_Real st
for x1, x2, x3, P, R, N being Nat
for V being Integer st x1 is odd & x2 is odd & P > 0 & N > (((sqrt x1) + (2 * (sqrt x2))) + (4 * (sqrt x3))) + R holds
( ( x1 is square & x2 is square & x3 is square & P divides R & V >= 0 ) iff ex z being Nat st
for f being Function of 8,F_Real st f = <%z,x1,(4 * x2),(16 * x3)%> ^ <%R,P,N,V%> holds
eval (K3,f) = 0 )