lagra4sq.miz



    begin

    definition

      let n be natural number;

      :: LAGRA4SQ:def1

      attr n is a_sum_of_four_squares means

      : Sum4Sq: ex n1,n2,n3,n4 be 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 :: LAGRA4SQ:1

    for n1,n2,n3,n4,m1,m2,m3,m4 be 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 be Nat such that

         A1: n = ((((n1 ^2 ) + (n2 ^2 )) + (n3 ^2 )) + (n4 ^2 )) by Sum4Sq;

        consider m1,m2,m3,m4 be 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;

      :: LAGRA4SQ:def2

      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 be Element of INT holds ex y be 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 be Function of INT , ( Segm p) such that

         A4: for x be 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;

      :: LAGRA4SQ:def3

      func LAG4SQf (v) -> FinSequence of INT means

      : Def2: ( len it ) = v & for i be 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) holds ex x be 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 be FinSequence of INT such that

         A2: ( dom f) = ( Seg v) & for k be 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;

      :: LAGRA4SQ:def4

      func LAG4SQg (v) -> FinSequence of INT means

      : Def3: ( len it ) = v & for i be 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 be Nat st k in ( Seg v) holds ex x be 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 be FinSequence of INT such that

         A2: ( dom f) = ( Seg v) & for k be 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 :: LAGRA4SQ:2

    

     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 :: LAGRA4SQ:3

    

     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 :: LAGRA4SQ:4

    

     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, INT_1: 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, INT_1: 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 :: LAGRA4SQ:5

    

     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, INT_1: 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, INT_1: 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

    theorem :: LAGRA4SQ:6

    

     Them1: 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 be 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 be 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 be object st x in A holds ex y be 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 be 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 be 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 :: LAGRA4SQ:7

    

     Them2: 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 :: LAGRA4SQ:8

    

     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 :: LAGRA4SQ:9

    

     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 :: LAGRA4SQ:10

    

     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 :: LAGRA4SQ:11

    

     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 :: LAGRA4SQ:12

    

     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 be Nat st P[h] & for n be 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 :: LAGRA4SQ:13

    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 :: LAGRA4SQ:14

    

     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 :: LAGRA4SQ:15

    

     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 :: LAGRA4SQ:16

    

     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

    theorem :: LAGRA4SQ:17

    

     Them8: for n be 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 be 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 be 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 be 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 be 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;

    ::$Notion-Name

    theorem :: LAGRA4SQ:18

    

     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