set M = the Jpolynom of 4, F_Complex ;
set Ree = F_Real ;
reconsider RR = F_Real as Field ;
consider K2 being INT -valued Polynomial of 6,F_Real such that
A1: for f being Function of 6,F_Real st f . 5 <> 0 holds
eval (K2,f) = ((power F_Real) . ((f /. 5),8)) * (eval ((Jsqrt the Jpolynom of 4, F_Complex ),(@ <%((- (f . 0)) + ((f . 4) / (f . 5))),(f . 1),(f . 2),(f . 3)%>))) and
A2: for f being INT -valued Function of 6,F_Real st f . 5 <> 0 & eval (K2,f) = 0 holds
f . 5 divides f . 4 by Th76;
consider K28 being Polynomial of (6 + 2),F_Real such that
A3: rng K28 c= (rng K2) \/ {(0. F_Real)} and
for b being bag of 6 + 2 holds
( b in Support K28 iff ( b | 6 in Support K2 & ( for i being Nat st i >= 6 holds
b . i = 0 ) ) ) and
for b being bag of 6 + 2 st b in Support K28 holds
K28 . b = K2 . (b | 6) and
A4: for x being Function of 6,F_Real
for y being Function of (6 + 2),F_Real st y | 6 = x holds
eval (K2,x) = eval (K28,y) by Th75;
rng K28 c= INT by A3, INT_1:def 2;
then reconsider K28 = K28 as INT -valued Polynomial of 8,F_Real by RELAT_1:def 19;
set nb = (EmptyBag 8) +* (6,1);
set n = Monom ((1. F_Real),((EmptyBag 8) +* (6,1)));
set vb = (EmptyBag 8) +* (7,1);
set v = Monom ((- (1. F_Real)),((EmptyBag 8) +* (7,1)));
set zb = (EmptyBag 8) +* (0,1);
set z = Monom ((1. F_Real),((EmptyBag 8) +* (0,1)));
reconsider v = Monom ((- (1. F_Real)),((EmptyBag 8) +* (7,1))) as INT -valued Polynomial of 8,F_Real ;
set znv = (Monom ((1. F_Real),((EmptyBag 8) +* (0,1)))) + ((Monom ((1. F_Real),((EmptyBag 8) +* (6,1)))) *' v);
reconsider K3 = Subst (K28,0,((Monom ((1. F_Real),((EmptyBag 8) +* (0,1)))) + ((Monom ((1. F_Real),((EmptyBag 8) +* (6,1)))) *' v))) as INT -valued Polynomial of 8,F_Real ;
take K3 ; :: thesis: 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 )
A6: ( 0 in Segm 6 & 1 in Segm 6 & 2 in Segm 6 & 3 in Segm 6 & 4 in Segm 6 & 5 in Segm 6 ) by NAT_1:44;
A7: ( 0 in Segm 8 & 1 in Segm 8 & 2 in Segm 8 & 3 in Segm 8 & 4 in Segm 8 & 5 in Segm 8 & 6 in Segm 8 & 7 in Segm 8 ) by NAT_1:44;
let x1, x2, x3, P, R, N be Nat; :: thesis: 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 )
let V be Integer; :: thesis: ( x1 is odd & x2 is odd & P > 0 & N > (((sqrt x1) + (2 * (sqrt x2))) + (4 * (sqrt x3))) + R implies ( ( 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 ) )
assume A8: ( x1 is odd & x2 is odd & P > 0 & N > (((sqrt x1) + (2 * (sqrt x2))) + (4 * (sqrt x3))) + R ) ; :: thesis: ( ( 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 )
thus ( x1 is square & x2 is square & x3 is square & P divides R & V >= 0 implies 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 ) :: thesis: ( 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 implies ( x1 is square & x2 is square & x3 is square & P divides R & V >= 0 ) )

proof

assume A9: ( x1 is square & x2 is square & x3 is square & P divides R & V >= 0 ) ; :: thesis: 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
then consider z1 being Integer such that
A10: - z1 = ((sqrt x1) + (2 * (sqrt x2))) + (4 * (sqrt x3)) and
A11: eval ((Jsqrt the Jpolynom of 4, F_Complex ),(@ <%z1,x1,(4 * x2),(16 * x3)%>)) = 0 by Th74;
consider d being Nat such that
A12: P * d = R by NAT_D:def 3, A9;
set zd = (- z1) + d;
A13: ( R / P = (d * P) / (P * 1) & (d * P) / (P * 1) = d / 1 & d / 1 = d ) by A12, A8, XCMPLX_1:91;
set f6 = ((((<%((- z1) + d)%> ^ <%x1%>) ^ <%(4 * x2)%>) ^ <%(16 * x3)%>) ^ <%R%>) ^ <%P%>;
reconsider F6 = @ (((((<%((- z1) + d)%> ^ <%x1%>) ^ <%(4 * x2)%>) ^ <%(16 * x3)%>) ^ <%R%>) ^ <%P%>) as Function of 6,F_Real ;
A14: ( F6 . 5 = P & F6 . 0 = (- z1) + d & F6 . 4 = R & F6 . 5 = P & F6 . 1 = x1 & F6 . 2 = 4 * x2 & F6 . 3 = 16 * x3 ) by AFINSQ_1:47;
A15: eval (K2,F6) = ((power F_Real) . ((F6 /. 5),8)) * (eval ((Jsqrt the Jpolynom of 4, F_Complex ),(@ <%((- (F6 . 0)) + ((F6 . 4) / (F6 . 5))),(F6 . 1),(F6 . 2),(F6 . 3)%>))) by A14, A1, A8
.= 0 by A11, A14, A13 ;
set zdv = ((- z1) + d) + (N * V);
set f8 = ((((((<%(((- z1) + d) + (N * V))%> ^ <%x1%>) ^ <%(4 * x2)%>) ^ <%(16 * x3)%>) ^ <%R%>) ^ <%P%>) ^ <%N%>) ^ <%V%>;
reconsider f = @ (((((((<%(((- z1) + d) + (N * V))%> ^ <%x1%>) ^ <%(4 * x2)%>) ^ <%(16 * x3)%>) ^ <%R%>) ^ <%P%>) ^ <%N%>) ^ <%V%>) as Function of 8,F_Real ;
set y = (((- z1) + d) + (N * V)) + (N * (- V));
reconsider Y = (((- z1) + d) + (N * V)) + (N * (- V)), zzR = ((- z1) + d) + (N * V), NR = N, VR = V as Element of F_Real by XREAL_0:def 1;
reconsider Yr = Y, zzr = zzR, Nr = NR, Vr = VR as Element of RR ;
( ((- z1) + d) + (N * V) is set & x1 is set & 4 * x2 is set & 16 * x3 is set & R is set & P is set & N is set & V is set ) by TARSKI:1;
then A16: ( f . 0 = ((- z1) + d) + (N * V) & f . 1 = x1 & f . 2 = 4 * x2 & f . 3 = 16 * x3 & f . 4 = R & f . 5 = P & f . 6 = N & f . 7 = V ) by AFINSQ_1:49;
A17: eval (((EmptyBag 8) +* (0,1)),f) = (power F_Real) . ((f . 0),1) by A7, Th14
.= zzR by GROUP_1:50, A16 ;
A18: eval ((Monom ((1. F_Real),((EmptyBag 8) +* (0,1)))),f) = (1. F_Real) * (eval (((EmptyBag 8) +* (0,1)),f)) by POLYNOM7:13
.= zzR by A17 ;
A19: eval (((EmptyBag 8) +* (7,1)),f) = (power F_Real) . ((f . 7),1) by A7, Th14
.= VR by GROUP_1:50, A16 ;
A20: eval (v,f) = (- (1. F_Real)) * (eval (((EmptyBag 8) +* (7,1)),f)) by POLYNOM7:13
.= - VR by A19
.= - Vr ;
A21: eval (((EmptyBag 8) +* (6,1)),f) = (power F_Real) . ((f . 6),1) by A7, Th14
.= NR by GROUP_1:50, A16 ;
A22: eval ((Monom ((1. F_Real),((EmptyBag 8) +* (6,1)))),f) = (1. F_Real) * (eval (((EmptyBag 8) +* (6,1)),f)) by POLYNOM7:13
.= Nr by A21 ;
A23: eval (((Monom ((1. F_Real),((EmptyBag 8) +* (6,1)))) *' v),f) = Nr * (- Vr) by A20, A22, POLYNOM2:25
.= multreal . (N,(- VR))
.= N * (- V) by BINOP_2:def 11 ;
A24: eval (((Monom ((1. F_Real),((EmptyBag 8) +* (0,1)))) + ((Monom ((1. F_Real),((EmptyBag 8) +* (6,1)))) *' v)),f) = (eval ((Monom ((1. F_Real),((EmptyBag 8) +* (0,1)))),f)) + (eval (((Monom ((1. F_Real),((EmptyBag 8) +* (6,1)))) *' v),f)) by POLYNOM2:23
.= (((- z1) + d) + (N * V)) + (N * (- V)) by A23, A18 ;
A25: ( dom (f +* (0,Y)) = 8 & 8 = dom f ) by PARTFUN1:def 2;
A26: Segm 6 c= Segm 8 by NAT_1:39;
then A27: dom ((f +* (0,Y)) | 6) = 6 by PARTFUN1:def 2;
for x being object st x in 6 holds
(((((<%((- z1) + d)%> ^ <%x1%>) ^ <%(4 * x2)%>) ^ <%(16 * x3)%>) ^ <%R%>) ^ <%P%>) . x = ((f +* (0,Y)) | 6) . x

proof

let x be object ; :: thesis: ( x in 6 implies (((((<%((- z1) + d)%> ^ <%x1%>) ^ <%(4 * x2)%>) ^ <%(16 * x3)%>) ^ <%R%>) ^ <%P%>) . x = ((f +* (0,Y)) | 6) . x )
assume A28: x in 6 ; :: thesis: (((((<%((- z1) + d)%> ^ <%x1%>) ^ <%(4 * x2)%>) ^ <%(16 * x3)%>) ^ <%R%>) ^ <%P%>) . x = ((f +* (0,Y)) | 6) . x
A29: x in Segm 6 by A28;
then reconsider x = x as Nat ;
A30: ((f +* (0,Y)) | 6) . x = (f +* (0,Y)) . x by A28, FUNCT_1:49;

per cases ( x = 0 or x <> 0 ) ;

suppose x = 0 ; :: thesis: (((((<%((- z1) + d)%> ^ <%x1%>) ^ <%(4 * x2)%>) ^ <%(16 * x3)%>) ^ <%R%>) ^ <%P%>) . x = ((f +* (0,Y)) | 6) . x

hence (((((<%((- z1) + d)%> ^ <%x1%>) ^ <%(4 * x2)%>) ^ <%(16 * x3)%>) ^ <%R%>) ^ <%P%>) . x = ((f +* (0,Y)) | 6) . x by A30, A14, A25, A28, A26, FUNCT_7:31; :: thesis: verum

end;

suppose A31: x <> 0 ; :: thesis: (((((<%((- z1) + d)%> ^ <%x1%>) ^ <%(4 * x2)%>) ^ <%(16 * x3)%>) ^ <%R%>) ^ <%P%>) . x = ((f +* (0,Y)) | 6) . x

then A32: (f +* (0,Y)) . x = f . x by FUNCT_7:32;
( x < 6 & 6 = 5 + 1 ) by A29, NAT_1:44;
then x <= 5 by NAT_1:13;
then not not x = 0 & ... & not x = 5 ;
hence (((((<%((- z1) + d)%> ^ <%x1%>) ^ <%(4 * x2)%>) ^ <%(16 * x3)%>) ^ <%R%>) ^ <%P%>) . x = ((f +* (0,Y)) | 6) . x by A31, A28, FUNCT_1:49, A16, A14, A32; :: thesis: verum

end;

end;

end;

then A33: (f +* (0,Y)) | 6 = F6 by PARTFUN1:def 2, A27;
eval (K3,f) = eval (K28,(f +* (0,Y))) by A24, Th37, A7;
then A34: eval (K3,f) = 0 by A15, A33, A4;
set zdv = ((- z1) + d) + (N * V);
reconsider zdv = ((- z1) + d) + (N * V) as Element of NAT by A9, A10, INT_1:3;
take Z = zdv; :: thesis: 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
let F be Function of 8,F_Real; :: thesis: ( F = <%Z,x1,(4 * x2),(16 * x3)%> ^ <%R,P,N,V%> implies eval (K3,F) = 0 )
assume A35: F = <%Z,x1,(4 * x2),(16 * x3)%> ^ <%R,P,N,V%> ; :: thesis: eval (K3,F) = 0
F = (((<%Z%> ^ <%x1%>) ^ <%(4 * x2)%>) ^ <%(16 * x3)%>) ^ <%R,P,N,V%> by A35, AFINSQ_1:def 14
.= (((<%Z%> ^ <%x1%>) ^ <%(4 * x2)%>) ^ <%(16 * x3)%>) ^ (((<%R%> ^ <%P%>) ^ <%N%>) ^ <%V%>) by AFINSQ_1:def 14
.= ((((<%Z%> ^ <%x1%>) ^ <%(4 * x2)%>) ^ <%(16 * x3)%>) ^ ((<%R%> ^ <%P%>) ^ <%N%>)) ^ <%V%> by AFINSQ_1:27
.= (((((<%Z%> ^ <%x1%>) ^ <%(4 * x2)%>) ^ <%(16 * x3)%>) ^ (<%R%> ^ <%P%>)) ^ <%N%>) ^ <%V%> by AFINSQ_1:27 ;
hence eval (K3,F) = 0 by A34, AFINSQ_1:27; :: thesis: verum

end;

given zz being Nat such that A36: for f being Function of 8,F_Real st f = <%zz,x1,(4 * x2),(16 * x3)%> ^ <%R,P,N,V%> holds
eval (K3,f) = 0 ; :: thesis: ( x1 is square & x2 is square & x3 is square & P divides R & V >= 0 )
<%zz,x1,(4 * x2),(16 * x3)%> ^ <%R,P,N,V%> = @ (<%zz,x1,(4 * x2),(16 * x3)%> ^ <%R,P,N,V%>) ;
then reconsider f = <%zz,x1,(4 * x2),(16 * x3)%> ^ <%R,P,N,V%> as INT -valued Function of 8,F_Real ;
A37: ( zz is set & x1 is set & 4 * x2 is set & 16 * x3 is set & R is set & P is set & N is set & V is set ) by TARSKI:1;
<%zz,x1,(4 * x2),(16 * x3)%> = ((<%zz%> ^ <%x1%>) ^ <%(4 * x2)%>) ^ <%(16 * x3)%> by AFINSQ_1:def 14;
then A38: f = (((<%zz%> ^ <%x1%>) ^ <%(4 * x2)%>) ^ <%(16 * x3)%>) ^ (((<%R%> ^ <%P%>) ^ <%N%>) ^ <%V%>) by AFINSQ_1:def 14
.= ((((<%zz%> ^ <%x1%>) ^ <%(4 * x2)%>) ^ <%(16 * x3)%>) ^ ((<%R%> ^ <%P%>) ^ <%N%>)) ^ <%V%> by AFINSQ_1:27
.= (((((<%zz%> ^ <%x1%>) ^ <%(4 * x2)%>) ^ <%(16 * x3)%>) ^ (<%R%> ^ <%P%>)) ^ <%N%>) ^ <%V%> by AFINSQ_1:27
.= ((((((<%zz%> ^ <%x1%>) ^ <%(4 * x2)%>) ^ <%(16 * x3)%>) ^ <%R%>) ^ <%P%>) ^ <%N%>) ^ <%V%> by AFINSQ_1:27 ;
then A39: ( f . 0 = zz & f . 1 = x1 & f . 2 = 4 * x2 & f . 3 = 16 * x3 & f . 4 = R & f . 5 = P & f . 6 = N & f . 7 = V ) by A37, AFINSQ_1:49;
A40: eval (K3,f) = 0 by A36;
A41: eval (K3,f) = eval (K28,(f +* (0,(eval (((Monom ((1. F_Real),((EmptyBag 8) +* (0,1)))) + ((Monom ((1. F_Real),((EmptyBag 8) +* (6,1)))) *' v)),f))))) by A7, Th37;
A42: dom f = Segm 8 by PARTFUN1:def 2;
set y = (- (N * V)) + zz;
reconsider Y = (- (N * V)) + zz, zzR = zz, NR = N, VR = V as Element of F_Real by XREAL_0:def 1;
reconsider Yr = Y, zzr = zzR, Nr = NR, Vr = VR as Element of RR ;
A43: eval (((EmptyBag 8) +* (0,1)),f) = (power F_Real) . ((f . 0),1) by A7, Th14
.= zzR by GROUP_1:50, A39 ;
A44: eval ((Monom ((1. F_Real),((EmptyBag 8) +* (0,1)))),f) = (1. F_Real) * (eval (((EmptyBag 8) +* (0,1)),f)) by POLYNOM7:13
.= zzR by A43 ;
A45: eval (((EmptyBag 8) +* (7,1)),f) = (power F_Real) . ((f . 7),1) by A7, Th14
.= VR by GROUP_1:50, A39 ;
A46: eval (v,f) = (- (1. F_Real)) * (eval (((EmptyBag 8) +* (7,1)),f)) by POLYNOM7:13
.= - VR by A45
.= - Vr ;
A47: eval (((EmptyBag 8) +* (6,1)),f) = (power F_Real) . ((f . 6),1) by A7, Th14
.= NR by GROUP_1:50, A39 ;
A48: eval ((Monom ((1. F_Real),((EmptyBag 8) +* (6,1)))),f) = (1. F_Real) * (eval (((EmptyBag 8) +* (6,1)),f)) by POLYNOM7:13
.= Nr by A47 ;
A49: eval (((Monom ((1. F_Real),((EmptyBag 8) +* (6,1)))) *' v),f) = Nr * (- Vr) by A46, A48, POLYNOM2:25
.= multreal . (N,(- VR))
.= N * (- V) by BINOP_2:def 11 ;
A50: eval (((Monom ((1. F_Real),((EmptyBag 8) +* (0,1)))) + ((Monom ((1. F_Real),((EmptyBag 8) +* (6,1)))) *' v)),f) = (eval ((Monom ((1. F_Real),((EmptyBag 8) +* (0,1)))),f)) + (eval (((Monom ((1. F_Real),((EmptyBag 8) +* (6,1)))) *' v),f)) by POLYNOM2:23
.= zz + (N * (- V)) by A49, A44 ;
set f6 = (f +* (0,Y)) | 6;
A51: ( ((f +* (0,Y)) | 6) . 0 = (f +* (0,Y)) . 0 & (f +* (0,Y)) . 0 = Y & ((f +* (0,Y)) | 6) . 1 = (f +* (0,Y)) . 1 & (f +* (0,Y)) . 1 = f . 1 & f . 1 = x1 & ((f +* (0,Y)) | 6) . 2 = (f +* (0,Y)) . 2 & (f +* (0,Y)) . 2 = f . 2 & f . 2 = 4 * x2 & ((f +* (0,Y)) | 6) . 3 = (f +* (0,Y)) . 3 & (f +* (0,Y)) . 3 = f . 3 & f . 3 = 16 * x3 & ((f +* (0,Y)) | 6) . 4 = (f +* (0,Y)) . 4 & (f +* (0,Y)) . 4 = f . 4 & f . 4 = R & ((f +* (0,Y)) | 6) . 5 = (f +* (0,Y)) . 5 & (f +* (0,Y)) . 5 = f . 5 & f . 5 = P ) by A38, A42, NAT_1:44, A6, FUNCT_1:49, FUNCT_7:31, FUNCT_7:32, A37, AFINSQ_1:49;
A52: rng ((f +* (0,Y)) | 6) c= the carrier of F_Real ;
Segm 6 c= Segm 8 by NAT_1:39;
then A53: dom ((f +* (0,Y)) | 6) = 6 by PARTFUN1:def 2;
then reconsider f6 = (f +* (0,Y)) | 6 as Function of 6,F_Real by A52, FUNCT_2:2;
rng (f +* (0,Y)) c= (rng f) \/ {((- (N * V)) + zz)} by FUNCT_7:100;
then rng (f +* (0,Y)) c= INT by INT_1:def 2;
then reconsider f6 = f6 as INT -valued Function of 6,F_Real ;
A54: f6 /. 5 <> 0 by A8, A51, A6, A53, PARTFUN1:def 6;
A55: eval (K2,f6) = 0 by A4, A50, A40, A41;
consider d being Nat such that
A56: P * d = R by NAT_D:def 3, A55, A51, A2, A8;
A57: ( R / P = (d * P) / (P * 1) & (d * P) / (P * 1) = d / 1 & d / 1 = d ) by A56, A8, XCMPLX_1:91;
A58: (power F_Real) . ((f6 /. 5),8) <> 0 by A54, Th6;
eval (K2,f6) = ((power F_Real) . ((f6 /. 5),8)) * (eval ((Jsqrt the Jpolynom of 4, F_Complex ),(@ <%((- (f6 . 0)) + ((f6 . 4) / (f6 . 5))),(f6 . 1),(f6 . 2),(f6 . 3)%>))) by A1, A8, A51;
then A59: eval ((Jsqrt the Jpolynom of 4, F_Complex ),(@ <%((- ((- (N * V)) + zz)) + d),x1,(4 * x2),(16 * x3)%>)) = 0 by A57, A51, A4, A50, A40, A41, A58;
then ( x1 is square & x2 is square & x3 is square & - ((- ((- (N * V)) + zz)) + d) <= ((sqrt x1) + (2 * (sqrt x2))) + (4 * (sqrt x3)) ) by A8, Th73;
then A60: ((- (N * V)) + (zz - d)) - (zz - d) <= (((sqrt x1) + (2 * (sqrt x2))) + (4 * (sqrt x3))) - (zz - d) by XREAL_1:9;
A61: ( sqrt x2 >= 0 & sqrt x3 >= 0 ) by SQUARE_1:def 2;
0 < sqrt x1 by A8, SQUARE_1:25;
then A62: 0 + 0 < (sqrt x1) + (((2 * (sqrt x2)) + (4 * (sqrt x3))) + R) by A61;
A63: (- (N * V)) / (- N) >= (((((sqrt x1) + (2 * (sqrt x2))) + (4 * (sqrt x3))) + d) - zz) / (- N) by A60, XREAL_1:73;
A64: (- (N * V)) / (- N) = V * ((- N) / (- N))
.= V * 1 by A62, A8, XCMPLX_1:60 ;
1 * d <= P * d by XREAL_1:64, NAT_1:14, A8;
then A65: ((((sqrt x1) + (2 * (sqrt x2))) + (4 * (sqrt x3))) - zz) + d <= ((((sqrt x1) + (2 * (sqrt x2))) + (4 * (sqrt x3))) - zz) + R by A56, XREAL_1:7;
((((sqrt x1) + (2 * (sqrt x2))) + (4 * (sqrt x3))) + R) - zz <= ((((sqrt x1) + (2 * (sqrt x2))) + (4 * (sqrt x3))) + R) - 0 by XREAL_1:10;
then ((((sqrt x1) + (2 * (sqrt x2))) + (4 * (sqrt x3))) - zz) + d <= (((sqrt x1) + (2 * (sqrt x2))) + (4 * (sqrt x3))) + R by A65, XXREAL_0:2;
then ((((sqrt x1) + (2 * (sqrt x2))) + (4 * (sqrt x3))) - zz) + d < N by A8, XXREAL_0:2;
then (((((sqrt x1) + (2 * (sqrt x2))) + (4 * (sqrt x3))) + d) - zz) / (- N) > N / (- N) by A62, A8, XREAL_1:75;
then V > N / (- N) by A63, A64, XXREAL_0:2;
then V > - (N / N) by XCMPLX_1:188;
then V > - 1 by A62, A8, XCMPLX_1:60;
then V >= (- 1) + 1 by INT_1:7;
hence ( x1 is square & x2 is square & x3 is square & P divides R & V >= 0 ) by A59, A8, Th73, A55, A51, A2; :: thesis: verum