:: Lagrange's Four-Square Theorem
::  by Yasushige Watase
:: 
:: Received June 4, 2014
:: Copyright (c) 2014-2018 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, SUBSET_1, 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;
 equalities ORDINAL1, SQUARE_1, FINSEQ_1;
 expansions TARSKI, XBOOLE_0, PBOOLE;
 theorems XBOOLE_0, AXIOMS, FUNCT_1, FUNCT_2, INT_1, NAT_1, NAT_D, NUMBERS,
      XXREAL_0, COMPLEX1, ABIAN, INT_2, XREAL_1, FINSEQ_1, NEWTON, INT_4,
      INT_6, CARD_1, CARD_2, RELAT_1, ORDINAL1, FINSEQ_4, POLYFORM, PEPIN,
      XXREAL_1, XCMPLX_0, SQUARE_1, NAT_3, XBOOLE_1, PRE_POLY, TARSKI;
 schemes FUNCT_2, FINSEQ_1, NAT_1;

begin :: Preliminaries

definition let n be natural number;
  attr n is a_sum_of_four_squares means :Sum4Sq:
    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;
  existence
  proof
    take n = 0;
    take 0,0,0,0;
    thus thesis;
  end;
end;

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

theorem :: 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;
  coherence
  proof
    consider n1,n2,n3,n4 being Nat such that
A1: n = n1^2 + n2^2 + n3^2 + n4^2 by Sum4Sq;
    consider m1,m2,m3,m4 being Nat such that
A2: m = m1^2 + m2^2 + m3^2 + m4^2 by Sum4Sq;
WW: n * m =
    (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 by A1,A2;
    set z1 = n1 * m1 - n2 * m2 - n3 * m3 - n4 * m4;
    set z2 = (n1 * m2 + n2 * m1 + n3 * m4 - n4 * m3);
    set z3 = (n1 * m3 - n2 * m4 + n3 * m1 + n4 * m2);
    set z4 = (n1 * m4 + n2 * m3 - n3 * m2 + n4 * m1);
    reconsider N1 = |. z1 .|, N2 = |. z2 .|, N3 = |. z3 .|, N4 = |. z4 .|
      as natural Number;
    reconsider N1,N2,N3,N4 as Nat by TARSKI:1;
    N1^2 = z1^2 & N2^2 = z2^2 & N3^2 = z3^2 & N4^2 = z4^2 by COMPLEX1:75;
    hence thesis by WW;
  end;
end;

registration
  cluster odd for prime Nat;
  existence by PEPIN:41,POLYFORM:6;
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   :Def1:
  for x be Element of INT holds it.x = x mod p;
  existence
  proof
    reconsider p as non zero Nat;
    defpred P[Element of INT,object] means $2 = $1 mod p;
A1: for x being Element of INT ex y being Element of Segm p st P[x,y]
    proof
    let i be Element of INT;
      i mod p >= 0 & i mod p < p by NAT_D:62; then
      reconsider j = i mod p as Element of NAT by INT_1:3;
A3:   j < p by NAT_D:62;
      reconsider j = i mod p as Element of Segm p by A3,NAT_1:44;
      take j;
      thus thesis;
    end;
    consider f being Function of INT, Segm p such that
A4: for x being Element of INT holds P[x,f.x] from FUNCT_2:sch 3(A1);
    thus thesis by A4;
  end;
  uniqueness
  proof
    let f,g be Function of INT, Segm p;
    assume that
A5: for x be Element of INT holds f.x = x mod p and
A6: for x be Element of INT holds g.x = x mod p;
    now
      let x be Element of INT;
      f.x = x mod p by A5;
      hence f.x = g.x by A6;
    end;
    hence thesis;
  end;
end;

definition let v;
  func LAG4SQf(v) -> FinSequence of INT means  :Def2:
   len it = v & for i being Nat st i in dom it holds it.i = (i -1)^2;
   existence
   proof
     defpred P[Nat,object] means $2 = ($1 -1)^2;
A1:  for k st k in Seg v ex x being Element of INT st P[k,x]
     proof
       let k;
       assume k in Seg v;
       reconsider j = (k - 1)^2 as Element of INT by INT_1:def 2;
       take j;
       thus thesis;
     end;
     consider f being FinSequence of INT such that
A2:  dom f = Seg v & for k being Nat st k in Seg v holds P[k,f.k]
     from FINSEQ_1:sch 5(A1);
     take f;
     Seg len f = Seg v by FINSEQ_1:def 3,A2;
     hence len f = v by FINSEQ_1:6;
     thus thesis by A2;
   end;
   uniqueness
   proof
     let z1,z2 be FinSequence of INT;
     assume that
A3:  len z1 = v and
A4:  for i st i in dom z1 holds z1.i = (i-1)^2 and
A5:  len z2 = v and
A6:  for i st i in dom z2 holds z2.i = (i-1)^2;
A7:  dom z1 = Seg len z1 by FINSEQ_1:def 3 .= dom z2 by A3,A5,FINSEQ_1:def 3;
     for x be Nat st x in dom z1 holds z1.x = z2.x
     proof
       let x be Nat;
       assume
A8:    x in dom z1; then
       reconsider x9 = x as Element of NAT;
       thus z1.x = (x9 -1)^2 by A4,A8 .= z2.x by A6,A7,A8;
     end;
     hence thesis by A7,FINSEQ_1:13;
   end;
end;

definition let v;
  func LAG4SQg(v) -> FinSequence of INT means  :Def3:
   len it = v & for i being Nat st i in dom it holds it.i = -1 - (i -1)^2;
  existence
  proof
     defpred P[Nat,object] means $2 = -1 - ($1 -1)^2;
A1:  for k being Nat st k in Seg v ex x being Element of INT st P[k,x]
     proof
       let k;
       assume k in Seg v;
       reconsider j = -1 - (k - 1)^2 as Element of INT by INT_1:def 2;
       take j;
       thus thesis;
     end;
     consider f being FinSequence of INT such that
A2:  dom f = Seg v & for k being Nat st k in Seg v holds P[k,f.k]
     from FINSEQ_1:sch 5(A1);
     take f;
     Seg len f = Seg v by A2,FINSEQ_1:def 3;
     hence len f = v by FINSEQ_1:6;
     thus thesis by A2;
   end;
   uniqueness
   proof
     let z1,z2 be FinSequence of INT;
     assume that
A3:  len z1 = v and
A4:  for i st i in dom z1 holds z1.i = -1 - (i-1)^2 and
A5:  len z2 = v and
A6:  for i st i in dom z2 holds z2.i = -1 - (i-1)^2;
A7:  dom z1 = Seg len z1 by FINSEQ_1:def 3 .= dom z2 by A3,A5,FINSEQ_1:def 3;
     for x be Nat st x in dom z1 holds z1.x = z2.x
    proof
      let x be Nat;
      assume
A8:   x in dom z1;
      thus z1.x = -1 - (x -1)^2 by A4,A8 .= z2.x by A6,A7,A8;
    end;
    hence thesis by A7,FINSEQ_1:13;
  end;
end;

theorem lem1:
  LAG4SQf(v) is one-to-one
  proof
    set f = LAG4SQf v;
    for n1, n2 be object st n1 in dom f & n2 in dom f
    & f.n1 = f.n2 holds n1 = n2
    proof
      let n1, n2 be object such that
A1:   n1 in dom f and
A2:   n2 in dom f and
A3:   f.n1 = f.n2;
A4:   dom f = Seg len f by FINSEQ_1:def 3.= Seg v by Def2;
      consider m1 be Nat such that
A5:   n1 = m1 and
A6:   1 <= m1 and
      m1 <= v by A1,A4;
      consider m2 be Nat such that
A7:   n2 = m2 and
A8:   1 <= m2 and
      m2 <= v by A2,A4;
      f.m1 = f.m2 implies m1 = m2
      proof
        assume
A11:    f.m1 = f.m2;
        assume
A12:    m1 <> m2;
A13:    f.m1 = (m1 - 1)^2 by Def2,A5,A1;
A14:    f.m1 - f.m2 =
        (m1 - 1)^2 -(m2 - 1)^2 by A13,Def2,A2,A7 .= (m2 + m1 - 2)*(m1 -m2);
A16:    m1 + m2 -2 > 0
        proof
          per cases by A8,XXREAL_0:1;
          suppose m2 = 1; then
            m1 > 1 by A12,A6,XXREAL_0:1; then
A17:        m1 + m2 > 1 + 1 by A8, XREAL_1:8;
            m1 + m2 + (-2) > 2 + (-2) by A17,XREAL_1:8;
            hence m1 + m2 -2 > 0;
          end;
          suppose m2 >1; then
A19:        m1 + m2 > 1 + 1 by A6,XREAL_1:8;
            m1 + m2 + (-2) > 2 + (-2) by A19,XREAL_1:8;
            hence m1 + m2 -2 > 0;
          end;
        end;
        m1 - m2 <> 0 by A12;
        hence contradiction by A11,A16,A14;
      end;
      hence thesis by A3,A5,A7;
    end;
    hence thesis by FUNCT_1:def 4;
  end;

theorem lem2:
  LAG4SQg v is one-to-one
    proof
      for n1, n2 be object st n1 in dom LAG4SQg v & n2 in dom LAG4SQg v
      & (LAG4SQg v).n1 = (LAG4SQg v).n2 holds n1 = n2
      proof
        let n1, n2 be object such that
A1:     n1 in dom LAG4SQg v and
A2:     n2 in dom LAG4SQg v and
A3:     (LAG4SQg v).n1 = (LAG4SQg v).n2;
A4:     dom LAG4SQg v = Seg len LAG4SQg v by FINSEQ_1:def 3
                       .= Seg v by Def3;
        consider m1 be Nat such that
A5:     n1 = m1 and
A6:     1 <= m1 and
        m1 <= v by A1,A4;
        consider m2 be Nat such that
A7:     n2 = m2 and
A8:     1 <= m2 and
        m2 <= v by A2,A4;
        (LAG4SQg v).m1 = (LAG4SQg v).m2 implies m1 = m2
        proof
          assume
A11:      (LAG4SQg v).m1 = (LAG4SQg v).m2;
          assume
A12:      m1 <> m2;
A13:      (LAG4SQg v).m1 = -1- (m1 - 1)^2 by Def3,A5,A1;
          (LAG4SQg v).m2 =-1 - (m2 - 1)^2 by Def3,A2,A7; then
A14:      (LAG4SQg v).m1 - (LAG4SQg v).m2 = (m2 + m1 - 2)*(m2 -m1) by A13;
A16:      m2 + m1 -2 > 0
          proof
            per cases by A8,XXREAL_0:1;
              suppose m2 = 1; then
A18:            m1 > 1 by A6,A12,XXREAL_0:1;
A19:            m1 + m2 > 1 + 1 by A8,A18, XREAL_1:8;
                m1 + m2 + (-2) > 2 + (-2) by A19,XREAL_1:8;
                hence thesis;
              end;
              suppose m2 >1; then
A20:            m1 + m2 > 1 + 1 by A6,XREAL_1:8;
                m1 + m2 + (-2) > 2 + (-2) by A20,XREAL_1:8;
                hence thesis;
              end;
          end;
          m2 - m1 <> 0 by A12;
          hence contradiction by A11,A14,A16;
          end;
          hence thesis by A5,A7,A3;
        end;
        hence thesis by FUNCT_1:def 4;
      end;

lem3:
  p > 2
  proof
    p > 1 by INT_2:def 4; then
    p >= 1 + 1 by INT_1:7;
    hence thesis by POLYFORM:5,XXREAL_0:1;
  end;

lem3a:
  p + 1 > 3
  proof
    p + 1 > 2 + 1 by lem3,XREAL_1:8;
    hence thesis;
  end;

 reserve a for Real;
 reserve b for Integer;

theorem lem4:
  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
     proof
       let p;
       consider s such that
A1:    p+1 = 2 * s by ABIAN:11;
       s > 0 by A1; then
       s in NAT by INT_1:3; then
       reconsider s as Nat;
A3:    2*(p - s) = p -1 by A1;
A4:    p -1 > 2 -1 by lem3, XREAL_1:14;
A5:    p - s > 0 by A3,A4;
A6:    p -s + s > 0 + s by A5,XREAL_1:8;
A7:    dom (LAG4SQf(s))=Seg len (LAG4SQf(s)) by FINSEQ_1:def 3
       .= Seg s by Def2;
       for j1, j2 be Integer st j1 in rng (LAG4SQf(s))
       & j2 in rng (LAG4SQf s) & j1 <> j2 holds j1 mod p <> j2 mod p
       proof
         let j1, j2 such that
A8:      j1 in rng (LAG4SQf s) and
A9:      j2 in rng (LAG4SQf s) and
A10:     j1 <> j2;
         consider i1 be object such that
A11:     i1 in dom (LAG4SQf s) and
A12:     j1 = (LAG4SQf s).i1 by A8,FUNCT_1:def 3;
         consider i2 be object such that
A13:     i2 in dom (LAG4SQf s) and
A14:     j2 = (LAG4SQf s).i2 by A9,FUNCT_1:def 3;
         reconsider i1,i2 as Nat by A11,A13;
A15:     j1 = (i1-1)^2 by A11,A12,Def2;
A16:     j2 = (i2-1)^2 by A13,A14,Def2;
A17:     j1 - j2 = (i1-1)^2 - (i2-1)^2 by A11,A12,A16,Def2
         .= (i1 + i2 -2)*(i1-i2);
A18:     j2 - j1 = (i2-1)^2 - (i1-1)^2 by A11,A12,A16,Def2
         .= (i2 + i1 -2)*(i2-i1);
         consider i9 be Nat such that
A19:     i1 = i9 and
A20:     1 <= i9 and
A21:     i9 <= s by A7,A11;
         consider i0 be Nat such that
A22:     i2 = i0 and
A23:     1 <= i0 and
A24:     i0 <= s by A7,A13;
A25:     i1 + i2 -2 < p
         proof
A26:       i1 + i2 <= s + s by A19,A21,A22,A24, XREAL_1:7;
           i1 + i2 + (-2) < p+1 + (-1) by A1,A26, XREAL_1:8;
           hence thesis;
         end;
A27:     i1 + i2 -2 > 0
         proof
           per cases by A22,A23,XXREAL_0:1;
           suppose i2 = 1; then
A29:         i1 > 1 by A10,A12,A14,A19,A20,XXREAL_0:1;
A30:         i1 + i2 > 1 + 1 by A22,A23,A29,XREAL_1:8;
             i1 + i2 + (-2) > 2 + (-2) by XREAL_1:8,A30;
             hence i1 + i2 -2 > 0;
           end;
           suppose i2 >1; then
A32:         i1 + i2 > 1 + 1 by A19,A20,XREAL_1:8;
             i1 + i2 + (-2) > 2 + (-2) by A32,XREAL_1:8;
             hence i1 + i2 -2 > 0;
           end;
         end;
A33:     i1 - i2 < p & i2 -i1 < p
         proof
           i1 - i2 <= i1 by XREAL_1:43; then
A34:       i1 - i2 <= s by A19,A21, XXREAL_0:2;
           i2 - i1 <= i2 by XREAL_1:43; then
           i2 - i1 <= s by A22,A24,XXREAL_0:2;
           hence thesis by A6,A34,XXREAL_0:2;
         end;
         j1 mod p <> j2 mod p
         proof
           per cases by A10,A12,A14,XXREAL_0:1;
             suppose i1 > i2; then
A39:         i1 - i2 > 0 by XREAL_1:50;
             reconsider i1,i2 as Nat;
A40:         i1 + i2 -2 in NAT by A27,INT_1:3;
A41:         i1 - i2 in NAT by A39, INT_1:3;
             (i1 + i2 -2)*(i1-i2) mod p <> 0
             proof
               assume (i1 + i2 -2)*(i1-i2) mod p = 0; then
A44:           (i1 + i2 -2)*(i1-i2) = p * ((i1 + i2 -2)*(i1-i2) div p) + 0
                 by A40,A41,NAT_D:2;
A45:           (i1 + i2 -2)*(i1-i2) div p in NAT by A40,A41,INT_1:3,55;
               p divides (i1 + i2 -2) or p divides (i1-i2)
               by A40,A41,A44,A45,NEWTON:80,NAT_D:def 3;
               hence contradiction by A25,A27,A33,A39,A40,A41,NAT_D:7;
             end;
             hence thesis by A15,A16,A17,INT_4:22;
             end;
             suppose i2 > i1; then
A47:           i2 - i1 > 0 by XREAL_1:50;
               reconsider i1,i2 as Nat;
               reconsider p as Nat;
A48:           i2 + i1 -2 in NAT by A27,INT_1:3;
A49:           i2 - i1 in NAT by A47,INT_1:3;
               (i2 + i1 -2)*(i2-i1) mod p <> 0
               proof
                 assume (i2 + i1 -2)*(i2-i1) mod p = 0; then
A52:             (i2 + i1 -2)*(i2-i1) = p * ((i2 + i1 -2)*(i2-i1) div p) + 0
                 by A48,A49,NAT_D:2;
A53:             (i2 + i1 -2)*(i2-i1) div p in NAT by A48,A49,INT_1:3,55;
                 p divides (i2 + i1 -2) or p divides (i2-i1)
                 by A48,A49,A52,A53,NEWTON:80,NAT_D:def 3;
                 hence contradiction by A25,A27,A47,A33,A48,A49,NAT_D:7;
               end;
               hence thesis by A15,A16,A18,INT_4:22;
             end;
         end;
         hence thesis;
       end;
       hence thesis by A1;
     end;

theorem lem5:
  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
    proof
      let p;
      consider s such that
A1:   p+1 = 2 * s by ABIAN:11;
      s > 0 by A1; then
      s in NAT by INT_1:3; then
      reconsider s as Nat;
A4:   2*(p - s) = p - 1 by A1;
      p -1 > 2 -1 by lem3, XREAL_1:14; then
      p - s > 0 by A4; then
A7:   p -s + s > 0 + s by XREAL_1:8;
A8:   dom LAG4SQg s = Seg len LAG4SQg s by FINSEQ_1:def 3
      .= Seg s by Def3;
      for j1, j2 st j1 in rng LAG4SQg s
      & j2 in rng LAG4SQg s & j1 <> j2 holds j1 mod p <> j2 mod p
      proof
        let j1, j2 such that
A9:     j1 in rng LAG4SQg s and
A10:    j2 in rng LAG4SQg s and
A11:    j1 <> j2;
        consider i1 be object such that
A12:    i1 in dom LAG4SQg s and
A13:    j1 = (LAG4SQg s).i1 by A9,FUNCT_1:def 3;
        consider i2 be object such that
A14:    i2 in dom (LAG4SQg s) and
A15:    j2 = (LAG4SQg s).i2 by A10,FUNCT_1:def 3;
        reconsider i1,i2 as Nat by A12,A14;
A16:    j2 = -1-(i2-1)^2 by A14,A15,Def3;
A17:    j2 - j1 = -1-(i2-1)^2 -(-1- (i1-1)^2) by A12,A13,A16,Def3
          .= (i1 + i2 -2)*(i1-i2);
A18:    j1 - j2 = -1-(i1-1)^2 - (-1-(i2-1)^2) by A12,A13,A16,Def3
          .= (i2 + i1 -2)*(i2-i1);
        consider i9 be Nat such that
A19:    i1 = i9 and
A20:    1 <= i9 and
A21:    i9 <= s by A8,A12;
        consider i0 be Nat such that
A28:    i2 = i0 and
A29:    1 <= i0 and
A30:    i0 <= s by A8,A14;
A31:    i1 + i2 -2 < p
        proof
          s + s = p+1 by A1; then
          i1 + i2 <= p+1 by A19,A21,A28,A30,XREAL_1:7; then
          i1 + i2 + -2 < p+1 + -1 by XREAL_1:8;
          hence thesis;
        end;
A34:    i1 + i2 -2 > 0
          proof
          per cases by A28,A29,XXREAL_0:1;
            suppose i2 = 1; then
            i1 > 1 by A11,A13,A15,A19,A20,XXREAL_0:1; then
            i1 + i2 > 1 + 1 by A28,A29,XREAL_1:8; then
            i1 + i2 + (-2) > 2 + (-2) by XREAL_1:8;
            hence i1 + i2 -2 > 0;
          end;
          suppose i2 > 1; then
            i1 + i2 > 1 + 1 by A19,A20,XREAL_1:8; then
            i1 + i2 + (-2) > 2 + (-2) by XREAL_1:8;
            hence i1 + i2 -2 > 0;
          end;
        end;
A40:    i1 - i2 < p & i2 -i1 < p
        proof
          i1 - i2 <= i1 by XREAL_1:43; then
A41:      i1 - i2 <= s by A19,A21,XXREAL_0:2;
          i2 - i1 <= i2 by XREAL_1:43; then
          i2 - i1 <= s by A28,A30,XXREAL_0:2;
          hence thesis by A7,A41,XXREAL_0:2;
        end;
        j1 mod p <> j2 mod p
        proof
          per cases by A11,A13,A15,XXREAL_0:1;
          suppose i1 > i2; then
A45:        i1 - i2 > 0 by XREAL_1:50;
            reconsider i1,i2 as Nat;
            reconsider p as Nat;
A46:        i1 + i2 -2 in NAT by A34,INT_1:3;
A47:        i1 - i2 in NAT by A45, INT_1:3;
A48:        (i1 + i2 -2)*(i1-i2) mod p <> 0
            proof
              assume
A49:          (i1 + i2 -2)*(i1-i2) mod p = 0;
A51:          (i1 + i2 -2)*(i1-i2) div p in NAT by A46,A47,INT_1:3,55;
              (i1 + i2 -2)*(i1-i2) = p*((i1 + i2 -2)*(i1-i2) div p)+0
                by A46,A47,A49,NAT_D:2; then
              p divides (i1 + i2 -2) or p divides (i1-i2)
                by A46,A47,A51,NAT_D:def 3,NEWTON:80;
              hence contradiction by A31,A34,A40,A45,A46,A47,NAT_D:7;
            end;
            j1 mod p = j2 mod p implies (j2 -j1) mod p = 0
            proof
              assume
A53:          j1 mod p = j2 mod p;
              (j2 - j1) mod p = ((j2 mod p) - (j1 mod p)) mod p by INT_6:7
                .= 0 by NAT_D:26,A53;
              hence thesis;
            end;
            hence thesis by A17,A48;
         end;
         suppose i2 > i1; then
A55:       i2 - i1 > 0 by XREAL_1:50;
A56:       i2 + i1 -2 in NAT by A34,INT_1:3;
A57:       i2 - i1 in NAT by A55,INT_1:3;
A58:       (i2 + i1 -2)*(i2-i1) mod p <> 0
           proof
             assume
A59:         (i2 + i1 -2)*(i2-i1) mod p = 0;
A61:         (i2 + i1 -2)*(i2-i1) div p in NAT by A56,A57,INT_1:3,55;
             (i2 + i1 -2)*(i2-i1) = p * ((i2 + i1 -2)*(i2-i1) div p) + 0
               by A56,A57,A59,NAT_D:2; then
             p divides (i2 + i1 -2) or p divides (i2-i1)
               by A56,A57,A61,NAT_D:def 3,NEWTON:80;
             hence contradiction by A31,A34,A40,A55,A56,A57,NAT_D:7;
          end;
          j1 mod p = j2 mod p implies (j1 -j2) mod p = 0
          proof
           assume
A63:       j1 mod p = j2 mod p;
           (j1 - j2) mod p = ((j1 mod p) - (j2 mod p)) mod p by INT_6:7
           .= 0 by NAT_D:26,A63;
           hence thesis;
         end;
         hence thesis by A18,A58;
       end;
     end;
     hence thesis;
     end;
     hence thesis by A1;
    end;

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

theorem Them1: :: 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
    proof
      let p;
      consider s such that
A1:   2*s = p+1 by ABIAN:11;
      s > 0 by A1;then
      s in NAT by INT_1:3; then
      reconsider s as Nat;
      set f = LAG4SQf(s);
      set g = LAG4SQg(s);
A5:   dom f = Seg len f by FINSEQ_1:def 3 .= Seg s by Def2;
A6:   dom g = Seg len g by FINSEQ_1:def 3 .= Seg s by Def3;
A7:   f is one-to-one by lem1;
A8:   g is one-to-one by lem2;
A9:   rng f misses rng g
      proof
        assume rng f meets rng g; then
        consider y be object such that
A12:    y in rng f & y in rng g by XBOOLE_0:3;
        consider i1 be object such that
A13:    i1 in dom f and
A14:    y = f.i1 by A12,FUNCT_1:def 3;
        consider i2 be object such that
A15:    i2 in dom g and
A16:    y = g.i2 by A12,FUNCT_1:def 3;
        reconsider i1,i2 as Nat by A13,A15;
        reconsider y as Integer by A14;
A17:    y = (i1 - 1)^2 by A13,Def2,A14;
        y = -1 - (i2 - 1)^2 by A15,Def3,A16;
        hence contradiction by A17;
      end;
A19:  card rng (g^f) = p+1
      proof
A20:    card rng f = card dom f by A7,CARD_1:70
          .= card (Seg len f) by FINSEQ_1:def 3 .= card (Seg s) by Def2
          .= s by FINSEQ_1:57;
A21:    card rng g = card dom g by A8,CARD_1:70
          .= card (Seg len g) by FINSEQ_1:def 3 .= card (Seg s) by Def3
          .= s by FINSEQ_1:57;
        card(rng(g^f)) = card (rng g \/ rng f) by FINSEQ_1:31
          .= card rng g +` card rng f by A9,CARD_2:35
          .= card (s +^ s) by CARD_2:def 1,A20,A21
          .= card (s + s) by CARD_2:36 .= p+1 by A1;
        hence thesis;
      end;
A23:  rng(g^f) = rng g \/ rng f by FINSEQ_1:31;
A24:  dom MODMAP_p = INT by FUNCT_2:def 1;
A25:  card dom ((MODMAP_p)|rng (g^f)) = p+1 by A19,A24,RELAT_1:62;
A26:  card rng ((MODMAP_p)|rng (g^f)) <= card Segm p by NAT_1:43;
      set s1 = card rng ((MODMAP_p)|rng (g^f));
      set t1 = card dom ((MODMAP_p)|rng (g^f));
      s1 < t1 by A25,A26,NAT_1:13; then
A28:  s1 in { i where i is Nat: i < t1 };
A29:  dom ((MODMAP_p)|rng (g^f)) <> {} by A25;
      set A = dom ((MODMAP_p)|rng (g^f));
      set B = rng ((MODMAP_p)|rng (g^f));
      defpred P[object,object] means
       ex m1 being Element of INT st $1 in A &
         $2=m1 & ((MODMAP_p)|rng (g^f)).$1 = m1;
A30:  card B in card A by A28,AXIOMS:4;
A31:  for x being object st x in A ex y being object st y in B & P[x,y]
      proof
        let x be object;
        assume
A32:    x in A;
        take y = ((MODMAP_p)|rng (g^f)).x;
        y in B by A32,FUNCT_1:3; then
        y in Segm p; then
        y in { i where i is Nat : i < p } by AXIOMS:4; then
        consider j be Nat such that
A36:    y = j & j < p;
        y in INT by A36,ORDINAL1:def 12, NUMBERS:17;
        hence thesis by FUNCT_1:3,A32;
      end;
      consider h be Function of A,B such that
A38:  for x being object st x in A holds P[x,h.x] from FUNCT_2:sch 1(A31);
      consider m1,m2 be object such that
A39:  m1 in A and
A40:  m2 in A and
A41:  m1 <> m2 and
A42:  h.m1 = h.m2 by A29,A30,RELAT_1:42,FINSEQ_4:65;
A43:  P[m1,h.m1] by A38,A39;
A44:  P[m2,h.m2] by A38,A40;
      reconsider m1,m2 as Element of INT by A39,A40;
A46:  ((MODMAP_p)|rng (g^f)).m1 = (MODMAP_p).m1 by A39,FUNCT_1:47
      .= m1 mod p by Def1;
A47:  ((MODMAP_p)|rng (g^f)).m2 = (MODMAP_p).m2 by A40,FUNCT_1:47
       .= m2 mod p by Def1;
A49:  A = dom (MODMAP_p) /\ rng (g^f) by RELAT_1:61
       .= rng (g^f) by A24,XBOOLE_1:28;
A50:   m1 in rng f implies m2 in rng g
       proof
         assume
A51:     m1 in rng f;
         assume not m2 in rng g; then
         m2 in rng f by A23,A40,A49,XBOOLE_0:def 3;
         hence contradiction by A1,A41,A47,A44,A42,A43,A46,A51,lem4;
       end;
A54:   m1 in rng g implies m2 in rng f
       proof
         assume
A55:     m1 in rng g;
         assume not m2 in rng f; then
         m2 in rng g by A23,A40,A49,XBOOLE_0:def 3;
         hence contradiction by A1,A41,A47,A44,A42,A43,A46,A55,lem5;
       end;
A58:   A = dom(MODMAP_p) /\ rng (g^f) by RELAT_1:61
       .= rng (g^f) by A24,XBOOLE_1:28;
       ex x1, x2, x3,x4,h be Nat st h > 0 & h < p &
       h*p = x1^2 + x2^2 + x3^2 + x4^2
       proof
A60:     p*p" = 1 by XCMPLX_0:def 7;
         per cases by A23,A39,A58,XBOOLE_0:def 3;
         suppose
A61:       m1 in rng f; then
           consider x0 be object such that
A62:       x0 in dom f and
A63:       m1 = f.x0 by FUNCT_1:def 3;
           reconsider x0 as Nat by A62;
A64:       m1 = (x0-1)^2 by Def2,A62,A63;
           consider y0 be object such that
A65:       y0 in dom g and
A66:       m2 = g.y0 by A50,A61,FUNCT_1:def 3;
           reconsider y0 as Nat by A65;
A67:       m2 = -1 - (y0-1)^2 by Def3,A65,A66;
           (m1 - m2) mod p = ((m1 mod p) - (m2 mod p)) mod p by INT_6:7
            .= 0 by A47,A44,A42,A43,A46,NAT_D:26; then
A69:       (m1 - m2) - ((m1 - m2) div p) * p = 0 by INT_1:def 10;
A70:       (m1 - m2) div p > 0 by A64,A67,A69;
           consider x9 be Nat such that
A71:       x0 = x9 and
A72:       1 <= x9 and
A73:       x9 <= s by A5,A62;
A74:       1-1 <= x9 - 1 by A72,XREAL_1:9;
           consider y9 be Nat such that
A75:       y0 = y9 and
A76:       1 <= y9 and
A77:       y9 <= s by A6,A65;
A78:       1-1 <= y9 - 1 by A76,XREAL_1:9;
           x9 - 1 <= s - 1 by A73,XREAL_1:9; then
A80:       (x9 - 1)^2 <= (s - 1)^2 by A74,XREAL_1:66;
           y9-1 <= s -1 by A77,XREAL_1:9; then
           (y9 - 1)^2 <= (s-1)^2 by A78,XREAL_1:66; then
           (x9 - 1)^2 + (y9 - 1)^2 <= (s-1)^2+(s-1)^2 by A80,XREAL_1:7; then
A84:       (x0 - 1)^2 + (y0 - 1)^2 + 1 <= (s-1)^2 + (s-1)^2 + 1
             by A71,A75,XREAL_1:7;
A85:       p^2 = (2*s -1)^2 by A1;
           2*s -2 > 3 -2 by A1,XREAL_1:9,lem3a; then
A86:       (s+1)*(2*s-2) > 0;
A87:       p^2 - ((s-1)^2 + (s-1)^2 + 1) + ((s-1)^2 + (s-1)^2 + 1)
           > 0 + ((s-1)^2 + (s-1)^2 + 1) by A85,A86,XREAL_1:6;
A89:       x0 -1 in NAT by A71,A74,INT_1:3;
A90:       y0 -1 in NAT by A75,A78,INT_1:3;
           set h = (m1 - m2) div p;
           h in NAT by A70,INT_1:3; then
           reconsider h as Nat;
A92:       h > 0 by A69,A64,A67;
           consider x1,x2,x3,x4 be Nat such that
A93:       x1 = x0 -1 and
A94:       x2 = y0 -1 and
A95:       x3 = 1 and
A96:       x4 = 0 by A89,A90;
A97:       (x0-1)^2 + (y0-1)^2 + 1 = x1^2 + x2^2 + x3^2 + x4^2
             by A96,A95,A94,A93;
           h*p < p*p by A69,A64,A67,A84,A87,XXREAL_0:2; then
           h*p*p" < p*p*p" by XREAL_1:68; then
           h*(p*p") < p*(p*p");
           hence thesis by A92,A69,A64,A67,A97,A60;
         end;
         suppose
A101:      m1 in rng g;
           consider x0 be object such that
A102:      x0 in dom f and
A103:      m2 = f.x0 by A54,A101,FUNCT_1:def 3;
           reconsider x0 as Nat by A102;
           consider y0 be object such that
A104:      y0 in dom g and
A105:      m1 = g.y0 by A101,FUNCT_1:def 3;
           reconsider y0 as Nat by A104;
A106:      m1 = -1 - (y0-1)^2 by A104,A105,Def3;
           (m2 - m1) mod p = ((m2 mod p) - (m1 mod p)) mod p by INT_6:7
           .= 0 by A47,A44,A42,A43,A46,NAT_D:26; then
           (m2 - m1) - ((m2 - m1) div p) * p = 0 by INT_1:def 10; then
A109:      (x0-1)^2-(-1-(y0-1)^2)=((m2-m1) div p) * p by A102,A103,A106,Def2;
A110:      (m2 - m1) div p >= 0 by A109;
           consider x9 be Nat such that
A111:      x0 = x9 and
A112:      1 <= x9 and
A113:      x9 <= s by A102,A5;
A114:      1-1 <= x9 - 1 by A112,XREAL_1:9;
           consider y9 be Nat such that
A115:      y0 = y9 and
A116:      1 <= y9 and
A117:      y9 <= s by A6,A104;
A118:      1-1 <= y9 - 1 by A116,XREAL_1:9;
           x9 - 1 <= s - 1 by A113,XREAL_1:9; then
A120:      (x9 - 1)^2 <=(s - 1)^2 by A114,XREAL_1:66;
           y9-1 <= s -1 by A117,XREAL_1:9; then
           (y9 - 1)^2 <=(s-1)^2 by A118,XREAL_1:66; then
           (x9 - 1)^2 + (y9-1)^2 <= (s-1)^2+(s-1)^2 by A120,XREAL_1:7; then
A124:      (x0 - 1)^2 + (y0-1)^2+1<=(s-1)^2+(s-1)^2+1 by A111,A115,XREAL_1:7;
A125:      p^2 = (2*s -1)^2 by A1;
           2*s -2 > 3 -2 by A1,XREAL_1:9,lem3a; then
           (s+1)*(2*s-2) > 0; then
A127:      p^2 - ((s-1)^2 + (s-1)^2 + 1) + ((s-1)^2 + (s-1)^2 + 1)
             > 0 + ((s-1)^2 + (s-1)^2 + 1) by A125,XREAL_1:6;
           set h = (m2 - m1) div p;
           h in NAT by A110,INT_1:3; then
           reconsider h as Nat;
A129:      x0 -1 in NAT by A114,A111,INT_1:3;
A130:      y0 -1 in NAT by INT_1:3, A115,A118;
A132:      h > 0 by A109;
           consider x1,x2,x3,x4 be Nat such that
A133:      x1 = x0 -1 & x2 = y0 -1 & x3 = 1 & x4 = 0 by A129,A130;
A134:      (x0-1)^2 + (y0-1)^2 + 1 = x1^2 + x2^2 + x3^2 + x4^2 by A133;
           h*p < p*p by A109,A124,A127,XXREAL_0:2; then
           h*p*p" < p*p*p" by XREAL_1:68; then
           h*(p*p") < p*(p*p");
           hence thesis by A60,A109,A132,A134;
         end;
       end;
       hence thesis;
     end;

theorem Them2: ::: 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
    proof
      let x1,h be Nat;
      assume
A1:   1 < h;
      reconsider h1 = h as Real;
      consider q1,r1 be Integer such that
A2:   x1 = (h*q1) + r1 and
A3:   0 <= r1 and
A4:   r1 < h by INT_4:13,A1;
A5:   r1 in [.0,h1.[ by A3,A4,XXREAL_1:3;
      h1/2 < h1 by A1,XREAL_1:216; then
A7:   [.0,h1.[ = [.0,h1/2.] \/ ].h1/2,h1.[ by XXREAL_1:169;
      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
      proof
        per cases by A5,A7,XBOOLE_0:def 3;
        suppose
A9:       r1 in [.0,h1/2.]; then
A10:      0 <= r1 & r1 <= h1/2 by XXREAL_1:1;
          r1 <= h1/2 & 0<= 2 by A9,XXREAL_1:1; then
A12:      2*r1 <= 2*(h1/2) by XREAL_1:64;
A13:      r1 in NAT by A10,INT_1:3;
          consider y1 be Integer such that
A14:      y1 = r1;
A15:      0 <= y1 & 2*y1 <= h1 by A9,A12,A14,XXREAL_1:1;
          h divides (x1 - y1) by A2,A14,INT_1:def 3; then
A17:      x1 mod h = y1 mod h by A1,A13,A14,INT_4:23;
          x1^2 mod h = ((x1 mod h)*(x1 mod h)) mod h by NAT_D:67 .=
            y1^2 mod h by NAT_D:67,A17;
          hence thesis by A1,A15,A17;
        end;
        suppose
A19:      r1 in ].h1/2,h1.[; then
A20:      h1/2 < r1 & r1 < h1 by XXREAL_1:4;
          r1 > 0 by A19,XXREAL_1:4; then
A22:      r1 in NAT by INT_1:3;
          set y1 = r1 - h;
          h divides (x1 - (y1 + h)) by A2,INT_1:def 3; then
A24:      x1 mod h = (y1 + h) mod h by A1,A22,INT_4:23
          .= ( (y1 mod h) + (h mod h)) mod h by NAT_D:66
          .= ( (y1 mod h) + 0) mod h by NAT_D:25
          .= y1 mod h by NAT_D:65;
A25:      x1^2 mod h = ((x1 mod h)*(x1 mod h)) mod h by NAT_D:67 .=
            y1^2 mod h by NAT_D:67,A24;
A26:      h1/2 -h < r1 - h by A20,XREAL_1:9;
          r1 - h < h1 - h by A20,XREAL_1:9; then
          2*(-h1/2) < 2*y1 & 2*y1 <= 2*(h1/2) by A26,XREAL_1:68;
          hence thesis by A24,A25;
        end;
      end;
      hence thesis;
    end;

theorem lem7:
  for i1,i2, c be Nat st i1 <= c & i2 <= c holds
    i1+i2 < 2*c or (i1 = c & i2 = c)
  proof
    let i1,i2, c be Nat;
    assume that
A1: i1 <= c and
A2: i2 <= c;
    i1 in [.0,c.] by A1,XXREAL_1:1; then
A3: i1 in [.0,c.[ or i1 = c by XXREAL_1:7;
    i2 in [.0,c.] by A2,XXREAL_1:1; then
A4: i2 in [.0,c.[ or i2 = c by XXREAL_1:7;
    per cases by A3,XXREAL_1:3,A4;
    suppose i1 = c & i2 = c;
      hence thesis;
    end;
    suppose 0 <= i1 & i1 < c & 0 <= i2 & i2 < c; then
      i1 + i2 < c + c by XREAL_1:8;
      hence thesis;
    end;
    suppose 0 <= i1 & i1 < c & i2 = c; then
      i1 + i2 < c + c by XREAL_1:8;
      hence thesis;
    end;
    suppose 0 <= i2 & i2 < c & i1 = c; then
      i1 + i2 < c + c by XREAL_1:8;
      hence thesis;
    end;
  end;

theorem lem8:
  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)
    proof
      let i1,i2,i3,i4, c be Nat;
      assume that
A1:   i1 <= c and
A2:   i2 <= c and
A3:   i3 <= c and
A4:   i4 <= c;
      per cases by A1,A2, A3,A4,lem7;
      suppose i1+i2 < 2*c & i3+i4 < 2*c; then
        (i1 + i2) + (i3 + i4) < 2*c +2*c by XREAL_1:8;
        hence thesis;
      end;
      suppose i1+i2 < 2*c & i3 = c & i4 = c; then
        (i1+i2) + (i3 +i4) < 2*c + 2*c by XREAL_1:8;
        hence thesis;
      end;
      suppose (i1 = c & i2 = c) & i3+i4 < 2*c; then
        (i1+i2) + (i3 +i4) < 2*c + 2*c by XREAL_1:8;
        hence thesis;
      end;
      suppose i1 = c & i2 = c & i3 = c & i4 = c;
        hence thesis;
      end;
    end;

theorem lem9:
  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
    proof
      let x1, h be Nat, y1 be Integer;
      assume that
A1:   1 < h and
A2:   x1 mod h = y1 mod h and
A3:   -h < 2*y1 and
A4:   (2*y1)^2 = h^2;
A7:   2*y1 = h by A3,A4,SQUARE_1:40;
      reconsider h as Integer;
      set h1 = h;
      y1 > 0 by A1,A3,A4,SQUARE_1:40; then
      y1 in NAT by INT_1:3; then
      h divides (x1 -y1) by A1,A2,INT_4:23; then
      consider m1 be Integer such that
A9:   (x1 - y1) = h*m1 by INT_1:def 3;
A10:  x1 = (2*m1 +1)*h1/2 by A7,A9;
A12:  (2*m1 +1)*(h1/2)*(h1/2)" >= 0*(h1/2)" by A7,A9;
      (h1/2)*(h1/2)" = 1 by A1,XCMPLX_0:def 7; then
      (2*m1 +1) = (2*m1 +1)*((h1/2)*(h1/2)"); then
      2*m1 +1 +(- 1) >= 0+(-1) by A12,XREAL_1:6; then
      2*m1*2" >= (-1)*2" by XREAL_1:64; then
      m1 > -1 by XXREAL_0:2; then
      m1 >= -1 +1 by INT_1:7; then
      m1 in NAT by INT_1:3;
      hence thesis by A3,A4,A10,SQUARE_1:40;
    end;

theorem lem10:
  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
  proof
    let x1, h be Nat, y1 be Integer;
    assume that
A1: 1 < h and
A2: x1 mod h = y1 mod h and
A3: y1 = 0;
A5: x1 mod h = 0 by NAT_D:26,A2,A3;
    reconsider x1 as Integer;
A6: h divides x1 by A1,A5,INT_1:62;
    reconsider h as Integer;
    thus thesis by A6,INT_1:def 3;
  end;

theorem Them5:
  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
    proof
      let p;
      let x1, x2,x3,x4, h be Nat;
      assume that
A1:   1 < h and
A2:   h < p and
A3:   h*p = x1^2 + x2^2 + x3^2 + x4^2;
      set h1 = h;
      consider y1 be Integer such that
A4:   x1 mod h = y1 mod h and
A5:   -h < 2*y1 and
A6:   2*y1 <= h and
A7:   x1^2 mod h = y1^2 mod h by A1,Them2;
      consider y2 be Integer such that
A8:   x2 mod h = y2 mod h and
A9:   -h < 2*y2 and
A10:  2*y2 <= h and
A11:  x2^2 mod h = y2^2 mod h by A1,Them2;
      consider y3 be Integer such that
A12:  x3 mod h = y3 mod h and
A13:  -h < 2*y3 and
A14:  2*y3 <= h and
A15:  x3^2 mod h = y3^2 mod h by A1,Them2;
      consider y4 be Integer such that
A16:  x4 mod h = y4 mod h and
A17:  -h < 2*y4 and
A18:  2*y4 <= h and
A19:  x4^2 mod h = y4^2 mod h by A1,Them2;
A20:  (x1^2 + x2^2) mod h = ((x1^2 mod h) +( x2^2 mod h)) mod h by NAT_D:66
      .= (y1^2 + y2^2) mod h by NAT_D:66,A11,A7;
A21:  (x3^2 + x4^2) mod h = ((x3^2 mod h) +( x4^2 mod h)) mod h by NAT_D:66
      .= (y3^2 + y4^2) mod h by NAT_D:66,A19,A15;
      0 = ((x1^2 + x2^2) + (x3^2 + x4^2)) mod h by A3,NAT_D:13
      .= (((x1^2 + x2^2) mod h) + ((x3^2 + x4^2) mod h)) mod h by NAT_D:66
      .= ((y1^2 + y2^2) + (y3^2 + y4^2)) mod h by NAT_D:66,A21,A20
      .= (y1^2 + y2^2 + y3^2 + y4^2) mod h; then
A22:  0 = (y1^2 + y2^2 + y3^2 + y4^2)-((y1^2 + y2^2 + y3^2 + y4^2) div h)*h
      by A1,INT_1:def 10;
      set r = (y1^2 + y2^2 + y3^2 + y4^2) div h;
      set z1 = x1*y1 + x2*y2 +x3*y3 + x4*y4;
      set z2 = -x1*y2 + x2*y1 - x3*y4 + x4*y3;
      set z3 = x1*y3 - x2*y4 - x3*y1 + x4*y2;
      set z4 = x1*y4 + x2*y3 - x3*y2 - x4*y1;
A25:  z1^2 + z2^2 + z3^2 + z4^2
      = (x1^2 + x2^2 +x3^2 + x4^2)*(y1^2 + y2^2 +y3^2 + y4^2)
      .= (h*p) * (r*h) by A22,A3 .= p*h^2*r;
A26:  x1^2 mod h = ((x1 mod h)*(x1 mod h)) mod h by NAT_D:67
        .= x1*y1 mod h by NAT_D:67,A4;
A27:  x2^2 mod h = ((x2 mod h)*(x2 mod h)) mod h by NAT_D:67
        .= x2*y2 mod h by NAT_D:67,A8;
A28:  x3^2 mod h = ((x3 mod h)*(x3 mod h)) mod h by NAT_D:67
        .= x3*y3 mod h by NAT_D:67,A12;
A29:  x4^2 mod h = ((x4 mod h)*(x4 mod h)) mod h by NAT_D:67
        .= x4*y4 mod h by NAT_D:67,A16;
A30:  (x1*y1 + x2*y2)mod h =((x1*y1 mod h) + (x2*y2 mod h)) mod h by NAT_D:66
      .= (x1^2 + x2^2) mod h by NAT_D:66,A27,A26;
A31:  (x3*y3 + x4*y4)mod h =((x3*y3 mod h) + (x4*y4 mod h)) mod h by NAT_D:66
      .= (x3^2 + x4^2) mod h by NAT_D:66,A29,A28;
A32:  z1 mod h = ((x1*y1+x2*y2)+(x3*y3+x4*y4)) mod h
      .= ( ((x1*y1+x2*y2) mod h)+ ((x3*y3 + x4*y4) mod h)) mod h by NAT_D:66
      .= ( (x1^2 + x2^2) + (x3^2 + x4^2)) mod h by NAT_D:66,A31,A30
      .= 0 by NAT_D:13,A3;
A33:  x1*y2 mod h = ((x1 mod h)*(y2 mod h)) mod h by NAT_D:67
      .= x1*x2 mod h by NAT_D:67,A8;
A34:  x2*y1 mod h = ((x2 mod h)*(y1 mod h)) mod h by NAT_D:67
      .= x2*x1 mod h by NAT_D:67,A4;
A35:  x3*y4 mod h = ((x3 mod h)*(y4 mod h)) mod h by NAT_D:67
      .= x3*x4 mod h by NAT_D:67,A16;
A36:  x4*y3 mod h = ((x4 mod h)*(y3 mod h)) mod h by NAT_D:67
      .= x4*x3 mod h by NAT_D:67,A12;
A37:  (-x1*y2 + x2*y1)mod h = (x2*y1 -x1*y2) mod h .=
      ((x2*y1 mod h) - (x1*y2 mod h)) mod h by INT_6:7 .=
      0 by NAT_D:26,A33,A34;
A38:  (- x3*y4 + x4*y3) mod h = (x4*y3 -x3*y4) mod h .=
      ((x4*x3 mod h) - (x3*x4 mod h)) mod h by A35,A36,INT_6:7
      .= 0 by NAT_D:26;
A39:  z2 mod h = ((-x1*y2 + x2*y1) + (-x3*y4 + x4*y3)) mod h
      .= (((-x1*y2+x2*y1) mod h)+((-x3*y4 + x4*y3) mod h)) mod h by NAT_D:66
      .= 0 by NAT_D:26,A38,A37;
A40:  x1*y3 mod h = ((x1 mod h)*(y3 mod h)) mod h by NAT_D:67
      .= x1*x3 mod h by NAT_D:67,A12;
A41:  x2*y4 mod h = ((x2 mod h)*(y4 mod h)) mod h by NAT_D:67
      .= x2*x4 mod h by NAT_D:67,A16;
A42:  x3*y1 mod h = ((x3 mod h)*(y1 mod h)) mod h by NAT_D:67
      .= x3*x1 mod h by NAT_D:67,A4;
A43:  x4*y2 mod h = ((x4 mod h)*(y2 mod h)) mod h by NAT_D:67
      .= x4*x2 mod h by NAT_D:67,A8;
A44:  (x1*y3 - x3*y1)mod h = ((x1*y3 mod h) - (x3*y1 mod h))mod h by INT_6:7
      .= 0 by NAT_D:26,A42,A40;
A45:  (x4*y2 - x2*y4) mod h = ((x4*y2 mod h) - (x2*y4 mod h))mod h by INT_6:7
      .= 0 by NAT_D:26,A41,A43;
A46:  z3 mod h = ((x1*y3 - x3*y1) + (x4*y2 - x2*y4)) mod h
      .= (((x1*y3 - x3*y1) mod h)+((x4*y2 - x2*y4) mod h)) mod h by NAT_D:66
      .= 0 by NAT_D:26,A45,A44;
A47:  x1*y4 mod h = ((x1 mod h)*(y4 mod h)) mod h by NAT_D:67
      .= x1*x4 mod h by NAT_D:67,A16;
A48:  x2*y3 mod h = ((x2 mod h)*(y3 mod h)) mod h by NAT_D:67
      .= x2*x3 mod h by NAT_D:67,A12;
A49:  x3*y2 mod h = ((x3 mod h)*(y2 mod h)) mod h by NAT_D:67
      .= x3*x2 mod h by NAT_D:67,A8;
A50:  x4*y1 mod h = ((x4 mod h)*(y1 mod h)) mod h by NAT_D:67
      .= x4*x1 mod h by NAT_D:67,A4;
A51:  (x1*y4 - x4*y1)mod h = ((x1*y4 mod h) - (x4*y1 mod h))mod h by INT_6:7
      .= 0 by NAT_D:26,A50,A47;
A52:  (x2*y3 - x3*y2) mod h = ((x2*y3 mod h) - (x3*y2 mod h))mod h by INT_6:7
      .= 0 by NAT_D:26,A49,A48;
A53:  z4 mod h = ((x1*y4 - x4*y1) + (x2*y3 - x3*y2)) mod h
      .= (((x1*y4 - x4*y1) mod h)+((x2*y3 - x3*y2) mod h)) mod h by NAT_D:66
      .= 0 by NAT_D:26,A52,A51;
      h divides z1 by A1,A32,INT_1:62; then
      consider t1 be Integer such that
A55:  z1 = h*t1 by INT_1:def 3;
      h divides z2 by A1,A39,INT_1:62; then
      consider t2 be Integer such that
A57:  z2 = h*t2 by INT_1:def 3;
      h divides z3 by A1,A46,INT_1:62; then
      consider t3 be Integer such that
A59:  z3 = h*t3 by INT_1:def 3;
      h divides z4 by A1,A53,INT_1:62; then
      consider t4 be Integer such that
A61:  z4 = h*t4 by INT_1:def 3;
A62:  h^2*p*r = (h*t1)^2+(h*t2)^2+(h*t3)^2+(h*t4)^2 by A61,A59,A57,A55,A25
      .= h1^2*(t1^2 + t2^2 + t3^2 + t4^2);
      (h^2)"*h^2 = 1 by A1,XCMPLX_0:def 7; then
A64:  p*r = (h^2)"*h^2 *p*r .=(h^2)"*(h^2 *p*r)
      .=(h^2)"* ( h^2*(t1^2 + t2^2 + t3^2 + t4^2)) by A62
      .=(h^2)"* h^2*(t1^2 + t2^2 + t3^2 + t4^2)
      .= 1*(t1^2 + t2^2 + t3^2 + t4^2) by A1,XCMPLX_0:def 7
      .= t1^2 + t2^2 + t3^2 + t4^2;
A65:  (2*y1)^2 <= h^2 by A5,A6,SQUARE_1:49;
A66:  (2*y2)^2 <= h^2 by A9,A10,SQUARE_1:49;
A67:  (2*y3)^2 <= h^2 by A13,A14,SQUARE_1:49;
A68:  (2*y4)^2 <= h^2 by A17,A18,SQUARE_1:49;
A69:  r <= h
      proof
A70:    4*y1^2 + 4*y2^2 <= h^2 + h^2 by A65,A66,XREAL_1:7;
        4*y3^2 + 4*y4^2 <= h^2 + h^2 by A67,A68,XREAL_1:7; then
        (4*y1^2 + 4*y2^2) + (4*y3^2 + 4*y4^2) <= (h^2 + h^2) + (h^2 + h^2)
          by A70,XREAL_1:7; then
        4"*(4*r*h) <= 4"*(4*h^2) by A22,XREAL_1:64;then
        (r*h)*h" <= (h^2)*h" by XREAL_1:64; then
A74:    r*(h*h") <= h*(h*h");
        h*h" = 1 by A1,XCMPLX_0:def 7;
        hence thesis by A74;
      end;
A76:  r <> h
      proof
        assume
A77:    r = h;
        per cases by A65,A66,A67,A68,lem8;
        suppose (2*y1)^2 + (2*y2)^2 + (2*y3)^2 + (2*y4)^2 < 4*h^2;
          hence contradiction by A22,A77;
        end;
        suppose that
A79:      (2*y1)^2 = h^2 and
A80:      (2*y2)^2 = h^2 and
A81:      (2*y3)^2 = h^2 and
A82:      (2*y4)^2 = h^2;
          reconsider h as Integer;
          reconsider h1 = h as Real;
A83:      h is even by A79;
          consider m1 be Nat such that
A84:      2*x1 = (2*m1 +1) * h by A1,A4,A5,A79,lem9;
          consider m2 be Nat such that
A85:      2*x2 = (2*m2 +1) * h by A1,A8,A9,A80,lem9;
          consider m3 be Nat such that
A86:      2*x3 = (2*m3 +1) * h by A1,A12,A13,A81,lem9;
          consider m4 be Nat such that
A87:      2*x4 = (2*m4 +1) * h by A1,A16,A17,A82,lem9;
          p*h1 = ((2*m1 +1) * h1/2)^2 + ((2*m2 +1) * h1/2)^2 +
           ((2*m3 +1) * h1/2)^2 + ((2*m4 +1) * h1/2)^2 by A84,A85,A86,A87,A3
          .= (m1^2+m1+m2^2+m2+m3^2+m3+m4^2+m4+1)*h1*h1; then
          p*h1*h1" = (m1^2+m1+m2^2+m2+m3^2+m3+m4^2+m4+1)*h1*h1*h1";then
A88:      p*(h1*h1") = (m1^2+m1+m2^2+m2+m3^2+m3+m4^2+m4+1)*h1*(h1*h1");
          h1*h1" = 1 by A1,XCMPLX_0:def 7;
          hence contradiction by A83,A88;
        end;
      end;
      reconsider x1 as Integer;
A90:  r <> 0
      proof
        assume r = 0; then
A92:    y1 = 0 & y2 = 0 & y3 = 0 & y4 = 0 by A22; then
        consider m1 be Integer such that
A93:    x1 = h*m1 by A1,A4,lem10;
        consider m2 be Integer such that
A94:    x2 = h*m2 by A1,A8,A92,lem10;
        consider m3 be Integer such that
A95:    x3 = h*m3 by A1,A12,A92,lem10;
        consider m4 be Integer such that
A96:    x4 = h*m4 by A1,A16,A92,lem10;
        h*p*h" = ((m1^2) + (m2^2) + (m3^2) + (m4^2))*h*h*h"
          by A93,A94,A95,A96,A3; then
A99:    (h*h")*p = ((m1^2) + (m2^2) + (m3^2) + (m4^2))*h*(h*h");
A100:   h*h" = 1 by A1,XCMPLX_0:def 7;
        reconsider p as Integer;
A101:   h divides p by A99,A100,INT_1:def 3;
        reconsider p as odd prime Nat;
        per cases by A101,INT_2:def 4;
        suppose h = 1;
          hence contradiction by A1;
        end;
        suppose h = p;
          hence contradiction by A2;
        end;
      end;
      r < h by A69,A76,XXREAL_0:1;
      hence thesis by A90,A64;
    end;

Them3:
  for p holds ex x1,x2,x3,x4 be Nat st p = x1^2 + x2^2 + x3^2 + x4^2
    proof
      let p;
      defpred P[Nat]
        means ex x1,x2,x3,x4 be Integer st 0 < $1 & $1 < p &
        $1*p = x1^2 + x2^2 + x3^2 + x4^2;
A1:   ex h be Nat st P[h]
      proof
        consider x1, x2,x3,x4, h1 be 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 thesis by A3,A4,A5;
      end;
A7:   ex h being Nat st P[h] & for n being Nat st P[n] holds h <= n from
        NAT_1:sch 5(A1);
      consider h0 be Nat such that
A8:   P[h0] and
A9:   for n be Nat st P[n] holds h0 <= n by A7;
      consider x1,x2,x3,x4 be 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;
        per cases by A19,XXREAL_0:1;
         suppose
A21:       h0 > 1;
           consider y1,y2,y3,y4 be Integer, h1 be 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;
         end;
         suppose h0 < 1;
           hence contradiction by A13;
         end;
      end;
      hence thesis by A11,A16;
    end;

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

Them4:
  for p be Prime st p is even holds
    ex x1, x2, x3, x4 be Nat st p = x1^2 + x2^2 + x3^2 + x4^2
  proof
    let p be Prime;
    assume
A1: p is even;
    reconsider p as Integer;
    set x1 = 1, x2 = 1, x3 = 0, x4 = 0;
    p = x1^2 + x2^2 + x3^2 + x4^2 by A1,ABIAN:def 1,INT_2:def 4;
    hence thesis;
  end;

theorem Them5:
  for p be Prime holds
    ex x1,x2,x3,x4 be Nat st p = x1^2 + x2^2 + x3^2 + x4^2
  proof
    let p be Prime;
    per cases;
    suppose p is even;
      hence thesis by Them4;
    end;
    suppose p is odd;
      hence thesis by Them3;
    end;
  end;

theorem Prime4Sq:
  for p1, p2 be Prime holds
    ex x1,x2,x3,x4 be Nat st p1*p2 = x1^2 + x2^2 + x3^2 + x4^2
  proof
    let p1, p2 be Prime;
    consider x1,x2,x3,x4 be Nat such that
A3: p1 = x1^2 + x2^2 + x3^2 + x4^2 by Them5;
    consider y1,y2,y3,y4 be Nat such that
A4: p2 = y1^2 + y2^2 + y3^2 + y4^2 by Them5;
    set z1 = x1*y1 + x2*y2 +x3*y3 + x4*y4,
        z2 = -x1*y2 + x2*y1 - x3*y4 + x4*y3,
        z3 = x1*y3 - x2*y4 - x3*y1 + x4*y2,
        z4 = x1*y4 + x2*y3 - x3*y2 - x4*y1;
    reconsider n1 = |. z1 .|, n2 = |. z2 .|, n3 = |. z3 .|,n4 = |. z4 .|
      as natural Number;
    reconsider n1,n2,n3,n4 as Nat by TARSKI:1;
A7: n1^2 = z1^2 & n2^2 = z2^2 & n3^2 = z3^2 & n4^2 = z4^2 by COMPLEX1:75;
    p1*p2 = z1^2 + z2^2 + z3^2 + z4^2 by A3,A4
       .= n1^2 + n2^2 + n3^2 + n4^2 by A7;
    hence thesis;
  end;

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

theorem Them7:
  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
  proof
    let p be Prime, n be Nat;
    defpred P[Nat] means ex x1,x2,x3,x4 be Nat
      st p|^$1 = x1^2 + x2^2 + x3^2 + x4^2;
A1: for n be Nat st P[n] holds P[n+1]
    proof
      let n be Nat; assume P[n]; then
      consider x1,x2,x3,x4 be Nat such that
A3:   p|^n = x1^2 + x2^2 + x3^2 + x4^2;
      consider y1,y2,y3,y4 be Nat such that
A4:   p = y1^2 + y2^2 + y3^2 + y4^2 by Them5;
      set z1 = x1*y1 + x2*y2 +x3*y3 + x4*y4,
          z2 = -x1*y2 + x2*y1 - x3*y4 + x4*y3,
          z3 = x1*y3 - x2*y4 - x3*y1 + x4*y2,
          z4 = x1*y4 + x2*y3 - x3*y2 - x4*y1;
      reconsider n1 = |. z1 .|, n2 = |. z2 .|, n3 = |. z3 .|, n4 = |. z4 .|
        as natural Number;
      reconsider n1,n2,n3,n4 as Nat by TARSKI:1;
A6:   n1^2 = z1^2 & n2^2 = z2^2 & n3^2 = z3^2 & n4^2 = z4^2 by COMPLEX1:75;
      p|^(n + 1) = p|^n * p by NEWTON:6
         .= z1^2 + z2^2 + z3^2 + z4^2 by A3,A4
         .= n1^2 + n2^2 + n3^2 + n4^2 by A6;
      hence thesis;
    end;
A8: P[0]
    proof
      consider x1,x2,x3,x4 be Nat such that
A9:   x1 = 1 & x2 = 0 & x3 = 0 & x4 = 0;
      p|^0 = x1^2 + x2^2 + x3^2 + x4^2 by A9,NEWTON:4;
      hence thesis;
    end;
    for n be Nat holds P[n] from NAT_1:sch 2(A8,A1);
    hence thesis;
  end;

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

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

theorem Them8:
  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
  proof
    let n be non zero Nat;
    defpred P[Nat] means for n being non zero Nat st card support ppf n = $1
      holds
    ex x1,x2,x3,x4 be Nat st Product ppf n = x1^2 + x2^2 + x3^2 + x4^2;
A1: P[ 0 ]
    proof
      let n be non zero Nat;
      assume card support ppf n = 0; then
      support ppf n = {}; then
A3:   ppf n = EmptyBag SetPrimes by PRE_POLY:81;
      set x1 = 1, x2 = 0, x3 = 0, x4 = 0;
      Product ppf n = x1^2 + x2^2 + x3^2 + x4^2 by A3,NAT_3:20;
      hence thesis;
    end;
A8: for k being Nat st P[k] holds P[k+1]
    proof
      let k be Nat;
      assume
A9:   P[k];
      let n be non zero Nat; assume
A10:  card support ppf n = k+1; then
      support ppf n is non empty set; then
      consider x be object such that
A11:  x in support ppf n by XBOOLE_0:def 1;
A12:  x in support pfexp n by A11,NAT_3:def 9;
A13:  x is Prime by A12,NAT_3:34;
      reconsider p = x as Nat by A12,NAT_3:34;
      set e = p |-count n;
      set s = p |^ e;
A14:  p > 1 by A13,INT_2:def 4;
      reconsider n as Integer;
      s divides n by A14,NAT_3:def 7; then
      consider t being Nat such that
A15:  n = s * t by NAT_D:def 3;
      reconsider n as Nat;
      reconsider s, t as non zero Nat by A15;
A16:  e = (p |-count s) + (p |-count t) by A13,NAT_3:28,A15
       .= e + (p |-count t) by A13,INT_2:def 4,NAT_3:25;
A17:  (p |-count t) = 0 by A16;
A19:  support ppf t = support pfexp t by NAT_3:def 9;
A20:  support ppf s = support pfexp s by NAT_3:def 9;
      (pfexp n).p = e by A13,NAT_3:def 8; then
      e <> 0 by A12,PRE_POLY:def 7; then
      support pfexp p|^e = {p} by A13,NAT_3:42; then
A21:  card support pfexp s = 1 by CARD_1:30;
      reconsider s1 = s, t1 = t as non zero Nat;
A22:  s1 gcd t1 = 1
      proof
        set u = s1 gcd t1;
        reconsider s1, t1 as Integer;
A23:    (s1 gcd t1) divides t1 by NAT_D:def 5;
        reconsider u as Integer;
        u <> 0 by INT_2:5; then
A24:    0+1 <= u by NAT_1:13;
        now assume s1 gcd t1 <> 1; then
          u > 1 by A24,XXREAL_0:1;then
          u >= 1+1 by NAT_1:13; then
          consider r being Element of NAT such that
A26:      r is prime and
A27:      r divides u by INT_2:31;
          u divides s1 by NAT_D:def 5; then
A28:      r divides s1 by A27,NAT_D:4;
          reconsider p as Integer;
A29:      r = 1 or r = p by A13,A26,A28,NAT_3:5,INT_2:def 4;
          reconsider p as Prime by A12,NAT_3:34;
          reconsider q = p as non zero Nat;
          1 = p |-count q by NAT_3:22,INT_2:def 4;
          hence contradiction
            by A17,A23,A27,A26,A29,INT_2:def 4,NAT_D:4,NAT_3:30;
        end;
        hence thesis;
      end;
       reconsider s1,t1 as Integer;
A31:   support ppf s misses support ppf t by A19,A20,A22,INT_2:def 3,NAT_3:44;
       reconsider n,t as non zero Nat;
A32:   k+1 = card support pfexp n by A10,NAT_3:def 9
       .= card support pfexp s + card support pfexp t
       by NAT_3:47,A22,INT_2:def 3,A15;
A33:   card support ppf t = k by A21,A32,NAT_3:def 9;
       consider x1,x2,x3,x4 be Nat such that
A34:   p |^ e = x1^2 + x2^2 + x3^2 + x4^2 by A13,Them7;
       consider y1,y2,y3,y4 be Nat such that
A35:   Product ppf t = y1^2 + y2^2 + y3^2 + y4^2 by A9,A33;
       set z1 = x1*y1 + x2*y2 +x3*y3 + x4*y4,
       z2 = -x1*y2 + x2*y1 - x3*y4 + x4*y3,
       z3 = x1*y3 - x2*y4 - x3*y1 + x4*y2,
       z4 = x1*y4 + x2*y3 - x3*y2 - x4*y1;
       reconsider n1 = |. z1 .|, n2 = |. z2 .|, n3 = |. z3 .|, n4 = |. z4 .|
         as natural Number;
       reconsider n1, n2, n3, n4 as Nat by TARSKI:1;
A37:   n1^2 = z1^2 & n2^2 = z2^2 & n3^2 = z3^2 & n4^2 = z4^2 by COMPLEX1:75;
       Product ppf n = Product (ppf s + ppf t) by A15,A22,INT_2:def 3,NAT_3:58
       .= (Product ppf s) * Product ppf t by NAT_3:19,A31
       .= (p |^ e)*Product ppf t by NAT_3:61
       .= z1^2 + z2^2 + z3^2 + z4^2 by A34,A35
       .= n1^2 + n2^2 + n3^2 + n4^2 by A37;
       hence thesis;
     end;
A38: for k be Nat holds P[k] from NAT_1:sch 2(A1,A8);
     reconsider n as non zero Nat;
A39: P[card support ppf n] by A38;
     consider x1,x2,x3,x4 be Nat such that
A40: Product ppf n = x1^2 + x2^2 + x3^2 + x4^2 by A39;
     thus thesis by A40;
   end;

::$N Lagrange's four-square theorem

theorem Lagrange4Squares:
  for n be Nat holds
    ex x1,x2,x3,x4 be Nat st n = x1^2 + x2^2 + x3^2 + x4^2
   proof
     let n be Nat;
     per cases;
     suppose n <> 0; then
       reconsider n as non zero Nat;
       consider x1,x2,x3,x4 be Nat such that
A1:    Product ppf n = x1^2 + x2^2 + x3^2 + x4^2 by Them8;
       n = x1^2 + x2^2 + x3^2 + x4^2 by A1,NAT_3:61;
       hence thesis;
     end;
     suppose
A2:    n = 0;
       set x1 = 0, x2 = 0, x3 = 0, x4 = 0;
       n = x1^2 + x2^2 + x3^2 + x4^2 by A2;
       hence thesis;
     end;
    end;

registration
  cluster -> a_sum_of_four_squares for Nat;
  coherence by Lagrange4Squares;
end;