let p1, p2 be Prime; ex x1, x2, x3, x4 being Nat st p1 * p2 = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)
consider x1, x2, x3, x4 being Nat such that
A3:
p1 = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)
by Them5;
consider y1, y2, y3, y4 being Nat such that
A4:
p2 = (((y1 ^2) + (y2 ^2)) + (y3 ^2)) + (y4 ^2)
by Them5;
set z1 = (((x1 * y1) + (x2 * y2)) + (x3 * y3)) + (x4 * y4);
set z2 = (((- (x1 * y2)) + (x2 * y1)) - (x3 * y4)) + (x4 * y3);
set z3 = (((x1 * y3) - (x2 * y4)) - (x3 * y1)) + (x4 * y2);
set z4 = (((x1 * y4) + (x2 * y3)) - (x3 * y2)) - (x4 * y1);
reconsider n1 = |.((((x1 * y1) + (x2 * y2)) + (x3 * y3)) + (x4 * y4)).|, n2 = |.((((- (x1 * y2)) + (x2 * y1)) - (x3 * y4)) + (x4 * y3)).|, n3 = |.((((x1 * y3) - (x2 * y4)) - (x3 * y1)) + (x4 * y2)).|, n4 = |.((((x1 * y4) + (x2 * y3)) - (x3 * y2)) - (x4 * y1)).| as natural Number ;
reconsider n1 = n1, n2 = n2, n3 = n3, n4 = n4 as Nat by TARSKI:1;
A7:
( n1 ^2 = ((((x1 * y1) + (x2 * y2)) + (x3 * y3)) + (x4 * y4)) ^2 & n2 ^2 = ((((- (x1 * y2)) + (x2 * y1)) - (x3 * y4)) + (x4 * y3)) ^2 & n3 ^2 = ((((x1 * y3) - (x2 * y4)) - (x3 * y1)) + (x4 * y2)) ^2 & n4 ^2 = ((((x1 * y4) + (x2 * y3)) - (x3 * y2)) - (x4 * y1)) ^2 )
by COMPLEX1:75;
p1 * p2 =
(((((((x1 * y1) + (x2 * y2)) + (x3 * y3)) + (x4 * y4)) ^2) + (((((- (x1 * y2)) + (x2 * y1)) - (x3 * y4)) + (x4 * y3)) ^2)) + (((((x1 * y3) - (x2 * y4)) - (x3 * y1)) + (x4 * y2)) ^2)) + (((((x1 * y4) + (x2 * y3)) - (x3 * y2)) - (x4 * y1)) ^2)
by A3, A4
.=
(((n1 ^2) + (n2 ^2)) + (n3 ^2)) + (n4 ^2)
by A7
;
hence
ex x1, x2, x3, x4 being Nat st p1 * p2 = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)
; verum