:: Lagrange's Four-Square Theorem
:: by Yasushige Watase
::
:: Received June 4, 2014
:: Copyright (c) 2014-2021 Association of Mizar Users


definition
let n be natural number ;
attr n is a_sum_of_four_squares means :Sum4Sq: :: LAGRA4SQ:def 1
ex n1, n2, n3, n4 being Nat st n = (((n1 ^2) + (n2 ^2)) + (n3 ^2)) + (n4 ^2);
end;

:: deftheorem Sum4Sq defines a_sum_of_four_squares LAGRA4SQ:def 1 :
for n being natural number holds
( n is a_sum_of_four_squares iff ex n1, n2, n3, n4 being Nat st n = (((n1 ^2) + (n2 ^2)) + (n3 ^2)) + (n4 ^2) );

registration
cluster epsilon-transitive epsilon-connected ordinal natural ext-real non negative V37() integer dim-like V48() cardinal complex a_sum_of_four_squares for set ;
existence
ex b1 being Nat st b1 is a_sum_of_four_squares
proof end;
end;

registration
let y be integer object ;
cluster |.y.| -> natural ;
coherence
|.y.| is natural
;
end;

theorem :: LAGRA4SQ:1
for n1, n2, n3, n4, m1, m2, m3, m4 being Nat holds ((((n1 ^2) + (n2 ^2)) + (n3 ^2)) + (n4 ^2)) * ((((m1 ^2) + (m2 ^2)) + (m3 ^2)) + (m4 ^2)) = (((((((n1 * m1) - (n2 * m2)) - (n3 * m3)) - (n4 * m4)) ^2) + (((((n1 * m2) + (n2 * m1)) + (n3 * m4)) - (n4 * m3)) ^2)) + (((((n1 * m3) - (n2 * m4)) + (n3 * m1)) + (n4 * m2)) ^2)) + (((((n1 * m4) + (n2 * m3)) - (n3 * m2)) + (n4 * m1)) ^2) ;

registration
let m, n be a_sum_of_four_squares Nat;
cluster m * n -> a_sum_of_four_squares ;
coherence
m * n is a_sum_of_four_squares
proof end;
end;

registration
cluster non empty epsilon-transitive epsilon-connected ordinal natural non zero ext-real positive non negative V37() integer dim-like V48() cardinal odd complex prime for set ;
existence
ex b1 being prime Nat st b1 is odd
by PEPIN:41, POLYFORM:6;
end;

definition
let p be odd prime Nat;
func MODMAP_ p -> Function of INT,(Segm p) means :Def1: :: LAGRA4SQ:def 2
for x being Element of INT holds it . x = x mod p;
existence
ex b1 being Function of INT,(Segm p) st
for x being Element of INT holds b1 . x = x mod p
proof end;
uniqueness
for b1, b2 being Function of INT,(Segm p) st ( for x being Element of INT holds b1 . x = x mod p ) & ( for x being Element of INT holds b2 . x = x mod p ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines MODMAP_ LAGRA4SQ:def 2 :
for p being odd prime Nat
for b2 being Function of INT,(Segm p) holds
( b2 = MODMAP_ p iff for x being Element of INT holds b2 . x = x mod p );

definition
let v be Nat;
func LAG4SQf v -> FinSequence of INT means :Def2: :: LAGRA4SQ:def 3
( len it = v & ( for i being Nat st i in dom it holds
it . i = (i - 1) ^2 ) );
existence
ex b1 being FinSequence of INT st
( len b1 = v & ( for i being Nat st i in dom b1 holds
b1 . i = (i - 1) ^2 ) )
proof end;
uniqueness
for b1, b2 being FinSequence of INT st len b1 = v & ( for i being Nat st i in dom b1 holds
b1 . i = (i - 1) ^2 ) & len b2 = v & ( for i being Nat st i in dom b2 holds
b2 . i = (i - 1) ^2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines LAG4SQf LAGRA4SQ:def 3 :
for v being Nat
for b2 being FinSequence of INT holds
( b2 = LAG4SQf v iff ( len b2 = v & ( for i being Nat st i in dom b2 holds
b2 . i = (i - 1) ^2 ) ) );

definition
let v be Nat;
func LAG4SQg v -> FinSequence of INT means :Def3: :: LAGRA4SQ:def 4
( len it = v & ( for i being Nat st i in dom it holds
it . i = (- 1) - ((i - 1) ^2) ) );
existence
ex b1 being FinSequence of INT st
( len b1 = v & ( for i being Nat st i in dom b1 holds
b1 . i = (- 1) - ((i - 1) ^2) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of INT st len b1 = v & ( for i being Nat st i in dom b1 holds
b1 . i = (- 1) - ((i - 1) ^2) ) & len b2 = v & ( for i being Nat st i in dom b2 holds
b2 . i = (- 1) - ((i - 1) ^2) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines LAG4SQg LAGRA4SQ:def 4 :
for v being Nat
for b2 being FinSequence of INT holds
( b2 = LAG4SQg v iff ( len b2 = v & ( for i being Nat st i in dom b2 holds
b2 . i = (- 1) - ((i - 1) ^2) ) ) );

theorem lem1: :: LAGRA4SQ:2
for v being Nat holds LAG4SQf v is one-to-one
proof end;

theorem lem2: :: LAGRA4SQ:3
for v being Nat holds LAG4SQg v is one-to-one
proof end;

lem3: for p being odd prime Nat holds p > 2
proof end;

lem3a: for p being odd prime Nat holds p + 1 > 3
proof end;

theorem lem4: :: LAGRA4SQ:4
for p being odd prime Nat
for s being Nat
for j1, j2 being Integer st 2 * s = p + 1 & j1 in rng (LAG4SQf s) & j2 in rng (LAG4SQf s) & not j1 = j2 holds
j1 mod p <> j2 mod p
proof end;

theorem lem5: :: LAGRA4SQ:5
for p being odd prime Nat
for s being Nat
for j1, j2 being Integer st 2 * s = p + 1 & j1 in rng (LAG4SQg s) & j2 in rng (LAG4SQg s) & not j1 = j2 holds
j1 mod p <> j2 mod p
proof end;

theorem Them1: :: LAGRA4SQ:6
for p being odd prime Nat ex x1, x2, x3, x4, h being Nat st
( 0 < h & h < p & h * p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) )
proof end;

theorem Them2: :: LAGRA4SQ:7
for x1, h being Nat st 1 < h holds
ex y1 being Integer st
( x1 mod h = y1 mod h & - h < 2 * y1 & 2 * y1 <= h & (x1 ^2) mod h = (y1 ^2) mod h )
proof end;

theorem lem7: :: LAGRA4SQ:8
for i1, i2, c being Nat st i1 <= c & i2 <= c & not i1 + i2 < 2 * c holds
( i1 = c & i2 = c )
proof end;

theorem lem8: :: LAGRA4SQ:9
for i1, i2, i3, i4, c being Nat st i1 <= c & i2 <= c & i3 <= c & i4 <= c & not ((i1 + i2) + i3) + i4 < 4 * c holds
( i1 = c & i2 = c & i3 = c & i4 = c )
proof end;

theorem lem9: :: LAGRA4SQ:10
for x1, h being Nat
for y1 being Integer st 1 < h & x1 mod h = y1 mod h & - h < 2 * y1 & (2 * y1) ^2 = h ^2 holds
( 2 * y1 = h & ex m1 being Nat st 2 * x1 = ((2 * m1) + 1) * h )
proof end;

theorem lem10: :: LAGRA4SQ:11
for x1, h being Nat
for y1 being Integer st 1 < h & x1 mod h = y1 mod h & y1 = 0 holds
ex m1 being Integer st x1 = h * m1
proof end;

theorem Them5: :: LAGRA4SQ:12
for p being odd Prime
for x1, x2, x3, x4, h being Nat st 1 < h & h < p & h * p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) holds
ex y1, y2, y3, y4 being Integer ex r being Nat st
( 0 < r & r < h & r * p = (((y1 ^2) + (y2 ^2)) + (y3 ^2)) + (y4 ^2) )
proof end;

Them3: for p being odd prime Nat ex x1, x2, x3, x4 being Nat st p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)
proof end;

theorem :: LAGRA4SQ:13
for p being Prime st p is even holds
p = 2 by ABIAN:def 1, INT_2:def 4;

Them4: for p being Prime st p is even holds
ex x1, x2, x3, x4 being Nat st p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)

proof end;

theorem Them5: :: LAGRA4SQ:14
for p being Prime ex x1, x2, x3, x4 being Nat st p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)
proof end;

theorem Prime4Sq: :: LAGRA4SQ:15
for p1, p2 being Prime ex x1, x2, x3, x4 being Nat st p1 * p2 = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)
proof end;

registration
let p1, p2 be Prime;
cluster p1 * p2 -> a_sum_of_four_squares ;
coherence
p1 * p2 is a_sum_of_four_squares
by Prime4Sq;
end;

theorem Them7: :: LAGRA4SQ:16
for p being Prime
for n being Nat ex x1, x2, x3, x4 being Nat st p |^ n = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)
proof end;

registration
let p be Prime;
let n be Nat;
cluster p |^ n -> a_sum_of_four_squares ;
coherence
p |^ n is a_sum_of_four_squares
by Them7;
end;

theorem Them8: :: LAGRA4SQ:17
for n being non zero Nat ex x1, x2, x3, x4 being Nat st Product (ppf n) = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)
proof end;

:: WP: Lagrange's four-square theorem
theorem Lagrange4Squares: :: LAGRA4SQ:18
for n being Nat ex x1, x2, x3, x4 being Nat st n = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)
proof end;

registration
cluster natural -> a_sum_of_four_squares for set ;
coherence
for b1 being Nat holds b1 is a_sum_of_four_squares
by Lagrange4Squares;
end;