let M be 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 )
let x1, x2, x3 be Nat; ( x1 is square & x2 is square & x3 is square implies ex z being Integer st
( - z = ((sqrt x1) + (2 * (sqrt x2))) + (4 * (sqrt x3)) & eval ((Jsqrt M),(@ <%z,x1,(4 * x2),(16 * x3)%>)) = 0 ) )
assume A1:
( x1 is square & x2 is square & x3 is square )
; ex z being Integer st
( - z = ((sqrt x1) + (2 * (sqrt x2))) + (4 * (sqrt x3)) & eval ((Jsqrt M),(@ <%z,x1,(4 * x2),(16 * x3)%>)) = 0 )
consider m1 being Nat such that
A2:
m1 ^2 = x1
by A1;
consider m2 being Nat such that
A3:
m2 ^2 = x2
by A1;
consider m3 being Nat such that
A4:
m3 ^2 = x3
by A1;
A5:
( sqrt x1 = m1 & sqrt x2 = m2 & sqrt x3 = m3 )
by A3, A4, A2, SQUARE_1:22;
take z = - ((m1 + (2 * m2)) + (4 * m3)); ( - z = ((sqrt x1) + (2 * (sqrt x2))) + (4 * (sqrt x3)) & eval ((Jsqrt M),(@ <%z,x1,(4 * x2),(16 * x3)%>)) = 0 )
reconsider A = {} as Subset of ((Seg 4) \ {1}) by XBOOLE_1:2;
set f = <%z,x1,(4 * x2),(16 * x3)%>;
set c = _sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>);
set F = <*z,x1,(4 * x2),(16 * x3)*>;
set AF = the addF of F_Complex;
set S = SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A);
A6:
XFS2FS <%z,x1,(4 * x2),(16 * x3)%> = <*z,x1,(4 * x2),(16 * x3)*>
by Lm1;
A7:
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 A8:
( 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 A6, Def11, CARD_1:def 7;
then A9:
( (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 A7, PARTFUN1:def 6, FINSEQ_3:25;
then A10:
SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A) = <*((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 A8, FINSEQ_4:76;
A11:
the addF of F_Complex = addcomplex
by COMPLFLD:def 1;
A12: 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 A11, A9, BINOP_2:def 3;
then A13:
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 A11, A9, BINOP_2:def 3;
A14:
( @ (@ <%z,x1,(4 * x2),(16 * x3)%>) = @ <%z,x1,(4 * x2),(16 * x3)%> & @ <%z,x1,(4 * x2),(16 * x3)%> = <%z,x1,(4 * x2),(16 * x3)%> )
;
( not 1 in A & 1 in dom (SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) & 2 in dom (SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) & 3 in dom (SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) & 4 in dom (SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) )
by A8, FINSEQ_3:25;
then A15:
( (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 & (SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) . 2 = (_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 = (_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)) . 3 & (SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) . 4 = (_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)) . 4 )
by HILB10_7:def 11;
A16:
( (_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 A6, Def11;
<*z,x1,(4 * x2),(16 * x3)*> . 2 = x1
;
then A17:
(_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)) . 2 = sqrt x1
by Th71, A6;
<*z,x1,(4 * x2),(16 * x3)*> . 3 = 4 * x2
;
then A18: (_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)) . 3 =
sqrt (4 * x2)
by Th71, A6
.=
2 * (sqrt x2)
by SQUARE_1:20, SQUARE_1:29
;
<*z,x1,(4 * x2),(16 * x3)*> . 4 = 16 * x3
;
then A19: (_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)) . 4 =
sqrt ((4 * 4) * x3)
by Th71, A6
.=
(sqrt (4 * 4)) * (sqrt x3)
by SQUARE_1:29
.=
(2 * 2) * (sqrt x3)
by SQUARE_1:20, SQUARE_1:29
;
A20:
not 4 is trivial
by NEWTON03:def 1;
the addF of F_Complex "**" (SignGen ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)), the addF of F_Complex,A)) = ((((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)) . 1) + ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)) . 2)) + ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)) . 3)) + ((_sqrt (XFS2FS <%z,x1,(4 * x2),(16 * x3)%>)) . 4)
by A13, A15, A10, A12, A11, BINOP_2:def 3;
hence
( - z = ((sqrt x1) + (2 * (sqrt x2))) + (4 * (sqrt x3)) & eval ((Jsqrt M),(@ <%z,x1,(4 * x2),(16 * x3)%>)) = 0 )
by A5, A14, A20, Th70, A16, A17, A18, A19; verum