let M be Jpolynom of 4, F_Complex ; :: thesis: 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)) )
let x1, x2, x3 be Nat; :: thesis: ( x1 is odd & x2 is odd implies 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)) ) )
assume A1: ( x1 is odd & x2 is odd ) ; :: thesis: 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)) )
set AF = the addF of F_Complex;
let z be Integer; :: thesis: ( eval ((Jsqrt M),(@ <%z,x1,(4 * x2),(16 * x3)%>)) = 0 implies ( x1 is square & x2 is square & x3 is square & - z <= ((sqrt x1) + (2 * (sqrt x2))) + (4 * (sqrt x3)) ) )
assume A2: eval ((Jsqrt M),(@ <%z,x1,(4 * x2),(16 * x3)%>)) = 0 ; :: thesis: ( x1 is square & x2 is square & x3 is square & - z <= ((sqrt x1) + (2 * (sqrt x2))) + (4 * (sqrt x3)) )
set f = <%z,x1,(4 * x2),(16 * x3)%>;
set F = <*z,x1,(4 * x2),(16 * x3)*>;
A3: XFS2FS <%z,x1,(4 * x2),(16 * x3)%> = <*z,x1,(4 * x2),(16 * x3)*> by Lm1;
not 4 is trivial by NEWTON03:def 1;
then consider A being Subset of ((Seg 4) \ {1}) such that
A4: the addF of F_Complex "**" (SignGen ((_sqrt (XFS2FS (@ (@ <%z,x1,(4 * x2),(16 * x3)%>)))), the addF of F_Complex,A)) = 0 by A2, Th70;
set c = _sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>);
set S = SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A);
A5: dom (SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) = dom (_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)) by HILB10_7:def 11;
len <*z,x1,(4 * x2),(16 * x3)*> = 4 by CARD_1:def 7;
then A6: ( len (SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) = len (_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)) & len (_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)) = 4 ) by A3, Def11, CARD_1:def 7;
then A7: ( (SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) /. 1 = (SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) . 1 & (SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) /. 2 = (SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) . 2 & (SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) /. 3 = (SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) . 3 & (SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) /. 4 = (SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) . 4 ) by A5, PARTFUN1:def 6, FINSEQ_3:25;
A8: the addF of F_Complex "**" <*((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) /. 1),((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) /. 2),((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) /. 3),((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) /. 4)*> = 0 by A7, A6, FINSEQ_4:76, A4;
set iz = 1;
( not 1 in A & 1 in dom (SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) ) by A6, ZFMISC_1:56, FINSEQ_3:25;
then A9: (SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) . 1 = (_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)) . 1 by HILB10_7:def 11;
consider i1 being Integer such that
A10: ( ( i1 = 1 or i1 = - 1 ) & (SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) . 2 = i1 * ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)) . 2) ) by Th72;
consider i2 being Integer such that
A11: ( ( i2 = 1 or i2 = - 1 ) & (SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) . 3 = i2 * ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)) . 3) ) by Th72;
consider i3 being Integer such that
A12: ( ( i3 = 1 or i3 = - 1 ) & (SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) . 4 = i3 * ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)) . 4) ) by Th72;
A13: ( (_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)) . 1 = <*z,x1,(4 * x2),(16 * x3)*> . 1 & <*z,x1,(4 * x2),(16 * x3)*> . 1 = z ) by A3, Def11;
<*z,x1,(4 * x2),(16 * x3)*> . 2 = x1 ;
then A14: (_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)) . 2 = sqrt x1 by Th71, A3;
<*z,x1,(4 * x2),(16 * x3)*> . 3 = 4 * x2 ;
then A15: (_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)) . 3 = sqrt (4 * x2) by Th71, A3
.= 2 * (sqrt x2) by SQUARE_1:20, SQUARE_1:29 ;
<*z,x1,(4 * x2),(16 * x3)*> . 4 = 16 * x3 ;
then A16: (_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)) . 4 = sqrt ((4 * 4) * x3) by Th71, A3
.= (sqrt (4 * 4)) * (sqrt x3) by SQUARE_1:29
.= (2 * 2) * (sqrt x3) by SQUARE_1:20, SQUARE_1:29 ;
A17: (sqrt x1) * (sqrt x1) = sqrt (x1 * x1) by SQUARE_1:29
.= sqrt (x1 ^2) by SQUARE_1:def 1
.= x1 by SQUARE_1:22 ;
A18: (sqrt x2) * (sqrt x2) = sqrt (x2 * x2) by SQUARE_1:29
.= sqrt (x2 ^2) by SQUARE_1:def 1
.= x2 by SQUARE_1:22 ;
A19: (sqrt x3) * (sqrt x3) = sqrt (x3 * x3) by SQUARE_1:29
.= sqrt (x3 ^2) by SQUARE_1:def 1
.= x3 by SQUARE_1:22 ;
A20: the addF of F_Complex = addcomplex by COMPLFLD:def 1;
A21: the addF of F_Complex "**" <*((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) /. 1),((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) /. 2),((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) /. 3),((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) /. 4)*> = the addF of F_Complex "**" (<*((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) /. 1),((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) /. 2),((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) /. 3)*> ^ <*((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) /. 4)*>) by FINSEQ_4:74
.= the addF of F_Complex . (( the addF of F_Complex "**" <*((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) /. 1),((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) /. 2),((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) /. 3)*>),((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) /. 4)) by FVSUM_1:8, FINSOP_1:4
.= the addF of F_Complex . (( the addF of F_Complex . (( the addF of F_Complex . (((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) /. 1),((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) /. 2))),((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) /. 3))),((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) /. 4)) by FINSOP_1:14 ;
the addF of F_Complex . (((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) /. 1),((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) /. 2)) = ((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) . 1) + ((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) . 2) by A20, A7, BINOP_2:def 3;
then the addF of F_Complex . (( the addF of F_Complex . (((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) /. 1),((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) /. 2))),((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) /. 3)) = (((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) . 1) + ((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) . 2)) + ((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) . 3) by A20, A7, BINOP_2:def 3;
then A22: 0 = ((((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) . 1) + ((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) . 2)) + ((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) . 3)) + ((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) . 4) by A21, A8, A20, A7, BINOP_2:def 3;
A23: (SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) . 1 <> 0

proof

assume (SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) . 1 = 0 ; :: thesis: contradiction
then (- (i1 * ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)) . 2))) * (- (i1 * ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)) . 2))) = (((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) . 3) + ((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) . 4)) * (((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) . 3) + ((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) . 4)) by A22, A10;
then A24: x1 = (((2 * 2) * x2) + (((i2 * i3) * 16) * ((sqrt x2) * (sqrt x3)))) + ((4 * 4) * x3) by A14, A15, A16, A17, A18, A19, A10, A11, A12;
then (x1 - (4 * x2)) - (16 * x3) = ((i2 * i3) * 16) * ((sqrt x2) * (sqrt x3)) ;
then reconsider ss = ((i2 * i3) * 16) * ((sqrt x2) * (sqrt x3)) as Integer ;
16 * 16 = 16 ^2 by SQUARE_1:def 1;
then ( ss ^2 = ss * ss & ss * ss = (16 ^2) * (x2 * x3) ) by A11, A12, A18, A19, SQUARE_1:def 1;
then 16 divides ss by Th3, INT_1:def 3;
then ex i being Integer st ss = 16 * i by INT_1:def 3;
hence contradiction by A1, A24; :: thesis: verum

end;

set Y = (((z * z) + (16 * x3)) - x1) - (4 * x2);
(((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) . 1) + ((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) . 4)) * (((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) . 1) + ((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) . 4)) = ((- ((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) . 2)) + (- ((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) . 3))) * ((- ((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) . 2)) + (- ((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) . 3))) by A22;
then A25: ((z * z) + ((((2 * (1 * i3)) * z) * 4) * (sqrt x3))) + ((4 * 4) * x3) = (x1 + ((2 * ((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) . 2)) * ((SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) . 3))) + ((2 * 2) * x2) by A14, A15, A17, A18, A10, A11, A13, A16, A19, A9, A12;
then A26: ((((z * z) + (16 * x3)) - x1) - (4 * x2)) + (((8 * (1 * i3)) * z) * (sqrt x3)) = ((4 * (i1 * i2)) * (sqrt x1)) * (sqrt x2) by A14, A15, A10, A11;
A27: (((z * z) + (16 * x3)) - x1) - (4 * x2) <> 0

proof

assume (((z * z) + (16 * x3)) - x1) - (4 * x2) = 0 ; :: thesis: contradiction
then ( (((2 * (1 * i3)) * z) * (sqrt x3)) * (((2 * (1 * i3)) * z) * (sqrt x3)) = (((2 * (1 * i3)) * z) * (sqrt x3)) ^2 & (((2 * (1 * i3)) * z) * (sqrt x3)) ^2 = (((i1 * i2) * (sqrt x1)) * (sqrt x2)) ^2 & (((i1 * i2) * (sqrt x1)) * (sqrt x2)) ^2 = (((i1 * i2) * (sqrt x1)) * (sqrt x2)) * (((i1 * i2) * (sqrt x1)) * (sqrt x2)) & z ^2 = z * z ) by A26, SQUARE_1:def 1;
then 2 * ((2 * (z ^2)) * x3) = x1 * x2 by A17, A18, A19, A10, A11, A12;
hence contradiction by A1; :: thesis: verum

end;

( (((((z * z) + (16 * x3)) - x1) - (4 * x2)) + (((8 * (1 * i3)) * z) * (sqrt x3))) * (((((z * z) + (16 * x3)) - x1) - (4 * x2)) + (((8 * (1 * i3)) * z) * (sqrt x3))) = (((((z * z) + (16 * x3)) - x1) - (4 * x2)) + (((8 * (1 * i3)) * z) * (sqrt x3))) ^2 & (((((z * z) + (16 * x3)) - x1) - (4 * x2)) + (((8 * (1 * i3)) * z) * (sqrt x3))) ^2 = (((4 * (i1 * i2)) * (sqrt x1)) * (sqrt x2)) ^2 & (((4 * (i1 * i2)) * (sqrt x1)) * (sqrt x2)) ^2 = (((4 * (i1 * i2)) * (sqrt x1)) * (sqrt x2)) * (((4 * (i1 * i2)) * (sqrt x1)) * (sqrt x2)) ) by A25, A14, A15, A10, A11, SQUARE_1:def 1;
then ((((((z * z) + (16 * x3)) - x1) - (4 * x2)) * ((((z * z) + (16 * x3)) - x1) - (4 * x2))) + (((((2 * ((((z * z) + (16 * x3)) - x1) - (4 * x2))) * 8) * (1 * i3)) * z) * (sqrt x3))) + (((z * z) * 64) * x3) = ((4 * 4) * x1) * x2 by A17, A18, A19, A10, A11, A12;
then ((((2 * ((((z * z) + (16 * x3)) - x1) - (4 * x2))) * 8) * (1 * i3)) * z) * (sqrt x3) = ((((4 * 4) * x1) * x2) - (((((z * z) + (16 * x3)) - x1) - (4 * x2)) * ((((z * z) + (16 * x3)) - x1) - (4 * x2)))) - (((z * z) * 64) * x3) ;
then reconsider Y1 = ((((2 * ((((z * z) + (16 * x3)) - x1) - (4 * x2))) * 8) * (1 * i3)) * z) * (sqrt x3) as Integer ;
((16 * ((((z * z) + (16 * x3)) - x1) - (4 * x2))) * z) ^2 = ((16 * ((((z * z) + (16 * x3)) - x1) - (4 * x2))) * z) * ((16 * ((((z * z) + (16 * x3)) - x1) - (4 * x2))) * z) by SQUARE_1:def 1;
then ( (((16 * ((((z * z) + (16 * x3)) - x1) - (4 * x2))) * z) ^2) * x3 = Y1 * Y1 & Y1 * Y1 = Y1 ^2 ) by A19, A12, SQUARE_1:def 1;
then (16 * ((((z * z) + (16 * x3)) - x1) - (4 * x2))) * z divides Y1 by Th3, INT_1:def 3;
then consider m being Integer such that
A28: ((16 * ((((z * z) + (16 * x3)) - x1) - (4 * x2))) * z) * m = Y1 by INT_1:def 3;
(16 * ((((z * z) + (16 * x3)) - x1) - (4 * x2))) * (z * m) = (16 * ((((z * z) + (16 * x3)) - x1) - (4 * x2))) * (((1 * i3) * z) * (sqrt x3)) by A28;
then z * m = ((1 * i3) * (sqrt x3)) * z by A27, XCMPLX_1:5;
then m = (1 * i3) * (sqrt x3) by A23, A13, A9, XCMPLX_1:5;
then ( - m = sqrt x3 or m = sqrt x3 ) by A12;
then reconsider S3 = sqrt x3 as Integer ;
sqrt x3 >= 0 by SQUARE_1:def 2;
then reconsider S3 = S3 as Element of NAT by INT_1:3;
set Z1 = (((1 * 2) * z) - 1) + ((i3 * 8) * S3);
A29: (((1 * 2) * z) - 1) + ((i3 * 8) * S3) <> 0

proof

assume (((1 * 2) * z) - 1) + ((i3 * 8) * S3) = 0 ; :: thesis: contradiction
then A30: ( (- (sqrt 1)) * (- (sqrt 1)) = (- (sqrt 1)) ^2 & (- (sqrt 1)) ^2 = (((2 * i1) * (sqrt x1)) + ((i2 * 4) * (sqrt x2))) ^2 & (((2 * i1) * (sqrt x1)) + ((i2 * 4) * (sqrt x2))) ^2 = (((2 * i1) * (sqrt x1)) + ((i2 * 4) * (sqrt x2))) * (((2 * i1) * (sqrt x1)) + ((i2 * 4) * (sqrt x2))) ) by SQUARE_1:def 1, A22, A13, A14, A15, A16, A9, A10, A11, A12;
then (1 - (4 * x1)) - (16 * x2) = ((16 * (i1 * i2)) * (sqrt x1)) * (sqrt x2) by A17, A18, A10, A11;
then reconsider ss = ((16 * (i1 * i2)) * (sqrt x1)) * (sqrt x2) as Integer ;
16 ^2 = 16 * 16 by SQUARE_1:def 1;
then ( ss ^2 = ss * ss & ss * ss = (16 ^2) * (x1 * x2) ) by A17, A18, A10, A11, SQUARE_1:def 1;
then 16 ^2 divides ss ^2 by INT_1:def 3;
then consider s being Integer such that
A31: 16 * s = ss by Th3, INT_1:def 3;
( (2 * 0) + 1 = 1 & 1 = 2 * (((2 * x1) + (8 * x2)) + (8 * s)) ) by A31, A30, A17, A18, A10, A11;
hence contradiction ; :: thesis: verum

end;

set Y1 = (((((((1 * 2) * z) - 1) + ((i3 * 8) * S3)) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) + (16 * x2)) - 1) - (4 * x1);
A32: ( ((- ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) - ((i2 * 4) * (sqrt x2))) * ((- ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) - ((i2 * 4) * (sqrt x2))) = ((- ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) - ((i2 * 4) * (sqrt x2))) ^2 & ((- ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) - ((i2 * 4) * (sqrt x2))) ^2 = ((sqrt 1) + ((2 * i1) * (sqrt x1))) ^2 & ((sqrt 1) + ((2 * i1) * (sqrt x1))) ^2 = ((sqrt 1) + ((2 * i1) * (sqrt x1))) * ((sqrt 1) + ((2 * i1) * (sqrt x1))) ) by SQUARE_1:def 1, A22, A13, A14, A15, A16, A9, A10, A11, A12;
A33: (((((((1 * 2) * z) - 1) + ((i3 * 8) * S3)) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) + (16 * x2)) - 1) - (4 * x1) <> 0

proof

assume (((((((1 * 2) * z) - 1) + ((i3 * 8) * S3)) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) + (16 * x2)) - 1) - (4 * x1) = 0 ; :: thesis: contradiction
then ( ((((2 * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) * i2) * 4) * (sqrt x2)) ^2 = ((((2 * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) * i2) * 4) * (sqrt x2)) * ((((2 * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) * i2) * 4) * (sqrt x2)) & ((((2 * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) * i2) * 4) * (sqrt x2)) * ((((2 * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) * i2) * 4) * (sqrt x2)) = (2 * ((2 * i1) * (sqrt x1))) * (2 * ((2 * i1) * (sqrt x1))) & (2 * ((2 * i1) * (sqrt x1))) * (2 * ((2 * i1) * (sqrt x1))) = (2 * ((2 * i1) * (sqrt x1))) ^2 ) by A32, A17, A10, A18, A11, SQUARE_1:def 1;
then ( (64 * (((((1 * 2) * z) - 1) + ((i3 * 8) * S3)) ^2)) * x2 = (64 * (((((1 * 2) * z) - 1) + ((i3 * 8) * S3)) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3)))) * x2 & (64 * (((((1 * 2) * z) - 1) + ((i3 * 8) * S3)) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3)))) * x2 = 16 * x1 ) by A17, A10, A18, A11, SQUARE_1:def 1;
then 2 * ((2 * (((((1 * 2) * z) - 1) + ((i3 * 8) * S3)) ^2)) * x2) = x1 ;
hence contradiction by A1; :: thesis: verum

end;

( (((((((((1 * 2) * z) - 1) + ((i3 * 8) * S3)) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) + (16 * x2)) - 1) - (4 * x1)) + ((((2 * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) * i2) * 4) * (sqrt x2))) * (((((((((1 * 2) * z) - 1) + ((i3 * 8) * S3)) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) + (16 * x2)) - 1) - (4 * x1)) + ((((2 * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) * i2) * 4) * (sqrt x2))) = (((((((((1 * 2) * z) - 1) + ((i3 * 8) * S3)) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) + (16 * x2)) - 1) - (4 * x1)) + ((((2 * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) * i2) * 4) * (sqrt x2))) ^2 & (((((((((1 * 2) * z) - 1) + ((i3 * 8) * S3)) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) + (16 * x2)) - 1) - (4 * x1)) + ((((2 * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) * i2) * 4) * (sqrt x2))) ^2 = (2 * ((2 * i1) * (sqrt x1))) ^2 & (2 * ((2 * i1) * (sqrt x1))) ^2 = (2 * ((2 * i1) * (sqrt x1))) * (2 * ((2 * i1) * (sqrt x1))) & ((((1 * 2) * z) - 1) + ((i3 * 8) * S3)) ^2 = ((((1 * 2) * z) - 1) + ((i3 * 8) * S3)) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3)) ) by A32, A17, A10, A18, A11, SQUARE_1:def 1;
then ((((((((((1 * 2) * z) - 1) + ((i3 * 8) * S3)) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) + (16 * x2)) - 1) - (4 * x1)) * ((((((((1 * 2) * z) - 1) + ((i3 * 8) * S3)) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) + (16 * x2)) - 1) - (4 * x1))) + ((((16 * ((((((((1 * 2) * z) - 1) + ((i3 * 8) * S3)) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) + (16 * x2)) - 1) - (4 * x1))) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) * i2) * (sqrt x2))) + ((64 * (((((1 * 2) * z) - 1) + ((i3 * 8) * S3)) ^2)) * x2) = 16 * x1 by A10, A17, A18, A11;
then (((16 * ((((((((1 * 2) * z) - 1) + ((i3 * 8) * S3)) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) + (16 * x2)) - 1) - (4 * x1))) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) * i2) * (sqrt x2) = ((16 * x1) - (((((((((1 * 2) * z) - 1) + ((i3 * 8) * S3)) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) + (16 * x2)) - 1) - (4 * x1)) * ((((((((1 * 2) * z) - 1) + ((i3 * 8) * S3)) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) + (16 * x2)) - 1) - (4 * x1)))) - ((64 * (((((1 * 2) * z) - 1) + ((i3 * 8) * S3)) ^2)) * x2) ;
then reconsider Y2 = (((16 * ((((((((1 * 2) * z) - 1) + ((i3 * 8) * S3)) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) + (16 * x2)) - 1) - (4 * x1))) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) * i2) * (sqrt x2) as Integer ;
( Y2 ^2 = Y2 * Y2 & Y2 * Y2 = (((16 * ((((((((1 * 2) * z) - 1) + ((i3 * 8) * S3)) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) + (16 * x2)) - 1) - (4 * x1))) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) * ((16 * ((((((((1 * 2) * z) - 1) + ((i3 * 8) * S3)) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) + (16 * x2)) - 1) - (4 * x1))) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3)))) * x2 & (((16 * ((((((((1 * 2) * z) - 1) + ((i3 * 8) * S3)) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) + (16 * x2)) - 1) - (4 * x1))) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) * ((16 * ((((((((1 * 2) * z) - 1) + ((i3 * 8) * S3)) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) + (16 * x2)) - 1) - (4 * x1))) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3)))) * x2 = (((16 * ((((((((1 * 2) * z) - 1) + ((i3 * 8) * S3)) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) + (16 * x2)) - 1) - (4 * x1))) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) ^2) * x2 ) by A18, A11, SQUARE_1:def 1;
then ((16 * ((((((((1 * 2) * z) - 1) + ((i3 * 8) * S3)) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) + (16 * x2)) - 1) - (4 * x1))) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) ^2 divides Y2 ^2 by INT_1:def 3;
then consider m1 being Integer such that
A34: ((16 * ((((((((1 * 2) * z) - 1) + ((i3 * 8) * S3)) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) + (16 * x2)) - 1) - (4 * x1))) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) * m1 = Y2 by Th3, INT_1:def 3;
((16 * ((((((((1 * 2) * z) - 1) + ((i3 * 8) * S3)) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) + (16 * x2)) - 1) - (4 * x1))) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) * m1 = ((16 * ((((((((1 * 2) * z) - 1) + ((i3 * 8) * S3)) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) + (16 * x2)) - 1) - (4 * x1))) * ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) * (i2 * (sqrt x2)) by A34;
then m1 = i2 * (sqrt x2) by A29, A33, XCMPLX_1:5;
then ( - m1 = sqrt x2 or m1 = sqrt x2 ) by A11;
then reconsider S2 = sqrt x2 as Integer ;
sqrt x2 >= 0 by SQUARE_1:def 2;
then reconsider S2 = S2 as Element of NAT by INT_1:3;
(2 * i1) * (sqrt x1) = ((- ((((1 * 2) * z) - 1) + ((i3 * 8) * S3))) - 1) - ((i2 * 4) * S2) by A22, A13, A14, A15, A16, A9, A10, A11, A12;
then reconsider Y3 = (2 * i1) * (sqrt x1) as Integer ;
( Y3 ^2 = Y3 * Y3 & Y3 * Y3 = (2 * 2) * x1 & (2 * 2) * x1 = (2 ^2) * x1 ) by A17, A10, SQUARE_1:def 1;
then 2 ^2 divides Y3 ^2 by INT_1:def 3;
then consider m2 being Integer such that
A35: 2 * m2 = Y3 by Th3, INT_1:def 3;
( ((2 * i1) * (sqrt x1)) * ((2 * i1) * (sqrt x1)) = ((2 * i1) * (sqrt x1)) ^2 & ((2 * i1) * (sqrt x1)) ^2 = Y3 * Y3 ) by SQUARE_1:def 1;
then (2 * 2) * x1 = (2 * 2) * (m2 * m2) by A35, A17, A10;
hence x1 is square ; :: thesis: ( x2 is square & x3 is square & - z <= ((sqrt x1) + (2 * (sqrt x2))) + (4 * (sqrt x3)) )
A36: ( sqrt x1 >= 0 & sqrt x2 >= 0 & sqrt x3 >= 0 ) by SQUARE_1:def 2;
( S2 ^2 = x2 & S3 ^2 = x3 ) by A18, A19, SQUARE_1:def 1;
hence ( x2 is square & x3 is square ) ; :: thesis: - z <= ((sqrt x1) + (2 * (sqrt x2))) + (4 * (sqrt x3))
A37: (i1 * (sqrt x1)) + ((i2 * 2) * (sqrt x2)) <= (1 * (sqrt x1)) + ((1 * 2) * (sqrt x2)) by A10, A36, XREAL_1:7, A11;
((i1 * (sqrt x1)) + ((i2 * 2) * (sqrt x2))) + ((i3 * 4) * (sqrt x3)) <= ((1 * (sqrt x1)) + (2 * (sqrt x2))) + (4 * (sqrt x3)) by A37, XREAL_1:7, A12, A36;
hence - z <= ((sqrt x1) + (2 * (sqrt x2))) + (4 * (sqrt x3)) by A22, A13, A14, A15, A16, A9, A10, A11, A12; :: thesis: verum