:: 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 b₁ being Nat st b₁ 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 b₁ being prime Nat st b₁ 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 b₁ being Function of INT,(Segm p) st
for x being Element of INT holds b₁ . x = x mod p

proof end;

uniqueness
for b₁, b₂ being Function of INT,(Segm p) st ( for x being Element of INT holds b₁ . x = x mod p ) & ( for x being Element of INT holds b₂ . x = x mod p ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines MODMAP_ LAGRA4SQ:def 2 :
for p being odd prime Nat
for b₂ being Function of INT,(Segm p) holds
( b₂ = MODMAP_ p iff for x being Element of INT holds b₂ . 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 b₁ being FinSequence of INT st
( len b₁ = v & ( for i being Nat st i in dom b₁ holds
b₁ . i = (i - 1) ^2 ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of INT st len b₁ = v & ( for i being Nat st i in dom b₁ holds
b₁ . i = (i - 1) ^2 ) & len b₂ = v & ( for i being Nat st i in dom b₂ holds
b₂ . i = (i - 1) ^2 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines LAG4SQf LAGRA4SQ:def 3 :
for v being Nat
for b₂ being FinSequence of INT holds
( b₂ = LAG4SQf v iff ( len b₂ = v & ( for i being Nat st i in dom b₂ holds
b₂ . 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 b₁ being FinSequence of INT st
( len b₁ = v & ( for i being Nat st i in dom b₁ holds
b₁ . i = (- 1) - ((i - 1) ^2) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of INT st len b₁ = v & ( for i being Nat st i in dom b₁ holds
b₁ . i = (- 1) - ((i - 1) ^2) ) & len b₂ = v & ( for i being Nat st i in dom b₂ holds
b₂ . i = (- 1) - ((i - 1) ^2) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines LAG4SQg LAGRA4SQ:def 4 :
for v being Nat
for b₂ being FinSequence of INT holds
( b₂ = LAG4SQg v iff ( len b₂ = v & ( for i being Nat st i in dom b₂ holds
b₂ . 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;

:: 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 b₁ being Nat holds b₁ is a_sum_of_four_squares by Lagrange4Squares;

end;