:: Lagrange's Four-Square Theorem
::  by Yasushige Watase
:: 
:: Received June 4, 2014
:: Copyright (c) 2014-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, CARD_1, FUNCT_1, RELAT_1, ARYTM_3, SUBSET_1, ARYTM_1,
      XXREAL_0, INT_2, NAT_1, INT_1, REAL_1, COMPLEX1, SQUARE_1, XCMPLX_0,
      ABIAN, FINSEQ_1, CARD_3, ORDINAL4, XBOOLE_0, CARD_2, ORDINAL2, XXREAL_1,
      NEWTON, NAT_3, PRE_POLY, LAGRA4SQ, ORDINAL1;
 notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2,
      BINOP_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, INT_1, NAT_1,
      FINSEQ_1, SQUARE_1, ARYTM_0, XREAL_0, INT_2, NAT_D, ABIAN, ARYTM_3,
      CARD_2, ORDINAL3, XTUPLE_0, XXREAL_1, PEPIN, ABSVALUE, PARTFUN1, NAT_3,
      PRE_POLY, VALUED_0, MEMBERED, NEWTON, RVSUM_1, UPROOTS, XXREAL_2;
 constructors ARYTM_2, RELSET_1, ARYTM_0, XXREAL_1, ORDINAL3, ABIAN, NAT_D,
      PEPIN, CARD_2, XXREAL_2, UPROOTS, NAT_3;
 registrations XBOOLE_0, XREAL_0, ORDINAL1, NAT_1, INT_1, FINSET_1, XXREAL_0,
      NEWTON, CARD_1, VALUED_0, RELSET_1, NUMBERS, XCMPLX_0, SQUARE_1, FUNCT_2,
      FINSEQ_1, ABIAN, NAT_3, PRE_POLY, PREPOWER;
 requirements REAL, NUMERALS, SUBSET, ARITHM;


begin :: Preliminaries

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

registration
  cluster a_sum_of_four_squares for Nat;
end;

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

theorem :: LAGRA4SQ:1 :: Lagrange identity
  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;
end;

registration
  cluster odd for prime Nat;
end;

 reserve i,j, k,v, w for Nat;
 reserve j1,j2, m, n, s, t, x, y for Integer;
 reserve p for odd prime Nat;

definition let p;
  func MODMAP_p -> Function of INT, Segm p means
:: LAGRA4SQ:def 2
  for x be Element of INT holds it.x = x mod p;
end;

definition let v;
  func LAG4SQf(v) -> FinSequence of INT means
:: LAGRA4SQ:def 3
   len it = v & for i being Nat st i in dom it holds it.i = (i -1)^2;
end;

definition let v;
  func LAG4SQg(v) -> FinSequence of INT means
:: LAGRA4SQ:def 4
   len it = v & for i being Nat st i in dom it holds it.i = -1 - (i -1)^2;
end;

theorem :: LAGRA4SQ:2
  LAG4SQf(v) is one-to-one;

theorem :: LAGRA4SQ:3
  LAG4SQg v is one-to-one;

 reserve a for Real;
 reserve b for Integer;

theorem :: LAGRA4SQ:4
  for p be odd prime Nat, s be Nat, j1, j2
     st 2*s = p+1 & j1 in rng LAG4SQf s & j2 in rng LAG4SQf s holds
     j1 = j2 or j1 mod p <> j2 mod p;

theorem :: LAGRA4SQ:5
  for p be odd prime Nat, s be Nat, j1, j2
    st 2*s = p+1 & j1 in rng LAG4SQg s & j2 in rng LAG4SQg s holds
    j1 = j2 or j1 mod p <> j2 mod p;

begin :: Any prime number can be expressed as the sum of four integer squares

theorem :: LAGRA4SQ:6  :: Lagrange lemma
  for p holds
    ex x1,x2,x3,x4, h be Nat st 0 < h & h < p &
    h*p = x1^2 + x2^2 + x3^2 + x4^2;

theorem :: LAGRA4SQ:7  ::: Lagrange Lemma
  for x1, h be Nat st 1 < h holds
    ex y1 be Integer st x1 mod h = y1 mod h & -h < 2*y1 & 2*y1 <= h &
    x1^2 mod h = y1^2 mod h;

theorem :: LAGRA4SQ:8
  for i1,i2, c be Nat st i1 <= c & i2 <= c holds
    i1+i2 < 2*c or (i1 = c & i2 = c);

theorem :: LAGRA4SQ:9
  for i1,i2,i3,i4, c be Nat st i1 <= c & i2 <= c & i3 <= c & i4 <= c holds
    i1+i2 + i3 + i4 < 4*c or (i1 = c & i2 = c & i3 = c & i4 = c);

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

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

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

theorem :: LAGRA4SQ:13
  for p be Prime st p is even holds p = 2;

theorem :: LAGRA4SQ:14
  for p be Prime holds
    ex x1,x2,x3,x4 be Nat st p = x1^2 + x2^2 + x3^2 + x4^2;

theorem :: LAGRA4SQ:15
  for p1, p2 be Prime holds
    ex x1,x2,x3,x4 be Nat st p1*p2 = x1^2 + x2^2 + x3^2 + x4^2;

registration let p1,p2 be Prime;
  cluster p1 * p2 -> a_sum_of_four_squares;
end;

theorem :: LAGRA4SQ:16
  for p be Prime, n be Nat holds
    ex x1,x2,x3,x4 be Nat st p|^n = x1^2 + x2^2 + x3^2 + x4^2;

registration let p be Prime, n be Nat;
  cluster p |^ n -> a_sum_of_four_squares;
end;

begin :: Proof of the Theorem of Sums of Four Squares

theorem :: LAGRA4SQ:17
  for n being non zero Nat holds
    ex x1,x2,x3,x4 be Nat st Product ppf n = x1^2 + x2^2 + x3^2 + x4^2;

::$N Lagrange's four-square theorem

theorem :: LAGRA4SQ:18
  for n be Nat holds
    ex x1,x2,x3,x4 be Nat st n = x1^2 + x2^2 + x3^2 + x4^2;

registration
  cluster -> a_sum_of_four_squares for Nat;
end;