:: by Yasushige Watase

::

:: Received June 4, 2014

:: Copyright (c) 2014-2021 Association of Mizar Users

:: 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) );

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

ex b_{1} being Nat st b_{1} is a_sum_of_four_squares
end;

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

proof 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
end;

registration

ex b_{1} being prime Nat st b_{1} is odd
by PEPIN:41, POLYFORM:6;

end;

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

definition

let p be odd prime Nat;

ex b_{1} being Function of INT,(Segm p) st

for x being Element of INT holds b_{1} . x = x mod p

for b_{1}, b_{2} being Function of INT,(Segm p) st ( for x being Element of INT holds b_{1} . x = x mod p ) & ( for x being Element of INT holds b_{2} . x = x mod p ) holds

b_{1} = b_{2}

end;
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 for x being Element of INT holds it . x = x mod p;

ex b

for x being Element of INT holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines MODMAP_ LAGRA4SQ:def 2 :

for p being odd prime Nat

for b_{2} being Function of INT,(Segm p) holds

( b_{2} = MODMAP_ p iff for x being Element of INT holds b_{2} . x = x mod p );

for p being odd prime Nat

for b

( b

definition

let v be Nat;

ex b_{1} being FinSequence of INT st

( len b_{1} = v & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = (i - 1) ^2 ) )

for b_{1}, b_{2} being FinSequence of INT st len b_{1} = v & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = (i - 1) ^2 ) & len b_{2} = v & ( for i being Nat st i in dom b_{2} holds

b_{2} . i = (i - 1) ^2 ) holds

b_{1} = b_{2}

end;
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 ( len it = v & ( for i being Nat st i in dom it holds

it . i = (i - 1) ^2 ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def2 defines LAG4SQf LAGRA4SQ:def 3 :

for v being Nat

for b_{2} being FinSequence of INT holds

( b_{2} = LAG4SQf v iff ( len b_{2} = v & ( for i being Nat st i in dom b_{2} holds

b_{2} . i = (i - 1) ^2 ) ) );

for v being Nat

for b

( b

b

definition

let v be Nat;

ex b_{1} being FinSequence of INT st

( len b_{1} = v & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = (- 1) - ((i - 1) ^2) ) )

for b_{1}, b_{2} being FinSequence of INT st len b_{1} = v & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = (- 1) - ((i - 1) ^2) ) & len b_{2} = v & ( for i being Nat st i in dom b_{2} holds

b_{2} . i = (- 1) - ((i - 1) ^2) ) holds

b_{1} = b_{2}

end;
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 ( len it = v & ( for i being Nat st i in dom it holds

it . i = (- 1) - ((i - 1) ^2) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def3 defines LAG4SQg LAGRA4SQ:def 4 :

for v being Nat

for b_{2} being FinSequence of INT holds

( b_{2} = LAG4SQg v iff ( len b_{2} = v & ( for i being Nat st i in dom b_{2} holds

b_{2} . i = (- 1) - ((i - 1) ^2) ) ) );

for v being Nat

for b

( b

b

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

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

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) )

( 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 )

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 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 )

( 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 )

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

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) )

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;

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 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;

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)

for n being Nat ex x1, x2, x3, x4 being Nat st p |^ n = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)

proof 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

registration
end;