let p be odd prime Nat; ex x1, x2, x3, x4 being Nat st p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)
defpred S1[ Nat] means ex x1, x2, x3, x4 being Integer st
( 0 < $1 & $1 < p & $1 * p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) );
A1:
ex h being Nat st S1[h]
proof
consider x1,
x2,
x3,
x4,
h1 being
Nat such that A3:
h1 > 0
and A4:
h1 < p
and A5:
h1 * p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)
by Them1;
thus
ex
h being
Nat st
S1[
h]
by A3, A4, A5;
verum
end;
A7:
ex h being Nat st
( S1[h] & ( for n being Nat st S1[n] holds
h <= n ) )
from NAT_1:sch 5(A1);
consider h0 being Nat such that
A8:
S1[h0]
and
A9:
for n being Nat st S1[n] holds
h0 <= n
by A7;
consider x1, x2, x3, x4 being Integer such that
A11:
h0 * p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)
by A8;
A13:
h0 >= 0 + 1
by A8, INT_1:7;
reconsider z1 = |.x1.|, z2 = |.x2.|, z3 = |.x3.|, z4 = |.x4.| as natural set by TARSKI:1;
A16:
( z1 ^2 = x1 ^2 & z2 ^2 = x2 ^2 & z3 ^2 = x3 ^2 & z4 ^2 = x4 ^2 )
by COMPLEX1:75;
h0 = 1
proof
assume A19:
h0 <> 1
;
contradiction
per cases
( h0 > 1 or h0 < 1 )
by A19, XXREAL_0:1;
suppose A21:
h0 > 1
;
contradictionconsider y1,
y2,
y3,
y4 being
Integer,
h1 being
Nat such that A23:
0 < h1
and A24:
h1 < h0
and A25:
h1 * p = (((y1 ^2) + (y2 ^2)) + (y3 ^2)) + (y4 ^2)
by A8, A11, A16, A21, Them5;
h1 < p
by A24, A8, XXREAL_0:2;
hence
contradiction
by A9, A23, A24, A25;
verum end; suppose
h0 < 1
;
contradictionhence
contradiction
by A13;
verum end;
end;
hence
ex x1, x2, x3, x4 being Nat st p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)
by A11, A16; verum