hilb10_1.miz



    begin

    reserve i,j,n,n1,n2,m,k,u for Nat,

r,r1,r2 for Real,

x,y for Integer,

a,b for non trivial Nat;

    

     Lm1: [\(((2 * n) + 1) / 2)/] = n

    proof

      (2 * n) < ((2 * n) + 1) by NAT_1: 13;

      then

       A1: n < (((2 * n) + 1) / 2) by XREAL_1: 81;

      ((2 * n) - 1) < ((2 * n) - 0 ) by XREAL_1: 15;

      then ((((2 * n) + 1) - 2) / 2) < n by XREAL_1: 83;

      then ((((2 * n) + 1) / 2) - (2 / 2)) < n;

      hence thesis by A1, INT_1:def 6;

    end;

    

     Lm2: [/(((2 * n) + 1) / 2)\] = (n + 1)

    proof

      ((2 * n) + 1) <= (((2 * n) + 1) + 1) by NAT_1: 11;

      then ((2 * n) + 1) <= (2 * (n + 1));

      then

       A1: (((2 * n) + 1) / 2) <= (n + 1) by XREAL_1: 79;

      (2 * n) < ((2 * n) + 1) by NAT_1: 13;

      then (n + 1) < ((((2 * n) + 1) / 2) + 1) by XREAL_1: 6, XREAL_1: 81;

      hence thesis by A1, INT_1:def 7;

    end;

    theorem :: HILB10_1:1

    

     Th1: for F be FinSequence of NAT st for k st 1 < k <= ( len F) holds ((F . k) mod n) = 0 holds (( Sum F) mod n) = ((F . 1) mod n)

    proof

      defpred P[ Nat] means for F be FinSequence of NAT st ( len F) = $1 & for k st 1 < k <= ( len F) holds ((F . k) mod n) = 0 holds (( Sum F) mod n) = ((F . 1) mod n);

      

       A1: P[ 0 ]

      proof

        let F be FinSequence of NAT such that

         A2: ( len F) = 0 ;

        F = {} by A2;

        hence thesis by RVSUM_1: 72;

      end;

      

       A3: P[k] implies P[(k + 1)]

      proof

        assume

         A4: P[k];

        set k1 = (k + 1);

        let F be FinSequence of NAT such that

         A5: ( len F) = (k + 1) and

         A6: for i be Nat st 1 < i <= ( len F) holds ((F . i) mod n) = 0 ;

        per cases ;

          suppose k = 0 ;

          then F = <*(F . 1)*> by A5, FINSEQ_1: 40;

          hence thesis;

        end;

          suppose

           A7: k > 0 ;

          F is non empty by A5;

          then ( len F) in ( dom F) by FINSEQ_5: 6;

          

          then ((F | k) ^ <*(F . k1)*>) = (F | k1) by A5, FINSEQ_5: 10

          .= F by A5;

          then

           A8: ( Sum F) = (( Sum (F | k)) + (F . k1)) by RVSUM_1: 74;

          

           A9: k <= k1 by NAT_1: 11;

          

           A10: ( len (F | k)) = k by A5, NAT_1: 11, FINSEQ_1: 59;

          for i be Nat st 1 < i <= ( len (F | k)) holds (((F | k) . i) mod n) = 0

          proof

            let i be Nat such that

             A11: 1 < i <= ( len (F | k));

            ((F | k) . i) = (F . i) & i <= ( len F) by A10, A11, A5, A9, FINSEQ_3: 112, XXREAL_0: 2;

            hence thesis by A11, A6;

          end;

          then

           A12: (( Sum (F | k)) mod n) = (((F | k) . 1) mod n) by A4, A10;

          

           A13: ((F . 1) mod n) = (( Sum (F | k)) mod n) by A7, NAT_1: 14, A12, FINSEQ_3: 112;

          per cases ;

            suppose n = 0 ;

            then (( Sum F) mod n) = 0 = ((F . 1) mod n) by INT_1:def 10;

            hence thesis;

          end;

            suppose

             A14: n > 0 ;

            

             A15: ( Sum (F | k)) is Nat & ( Sum F) is Nat by TARSKI: 1;

            ( 0 + 1) < k1 by A7, XREAL_1: 8;

            then 0 = ((( Sum F) - ( Sum (F | k))) mod n) by A5, A6, A8;

            hence thesis by A13, A15, A14, INT_4: 22;

          end;

        end;

      end;

       P[k] from NAT_1:sch 2( A1, A3);

      hence thesis;

    end;

    theorem :: HILB10_1:2

    

     Th2: for f be complex-valued FinSequence holds ex e,o be complex-valued FinSequence st ( len e) = [\(( len f) / 2)/] & ( len o) = [/(( len f) / 2)\] & ( Sum f) = (( Sum e) + ( Sum o)) & for n holds (e . n) = (f . (2 * n)) & (o . n) = (f . ((2 * n) - 1))

    proof

      defpred P[ Nat] means for f be complex-valued FinSequence st ( len f) = $1 holds ex e,o be complex-valued FinSequence st ( len e) = [\(( len f) / 2)/] & ( len o) = [/(( len f) / 2)\] & ( Sum f) = (( Sum e) + ( Sum o)) & for n holds (e . n) = (f . (2 * n)) & (o . n) = (f . ((2 * n) - 1));

      

       A1: P[ 0 ]

      proof

        let f be complex-valued FinSequence such that

         A2: ( len f) = 0 ;

        take f, f;

        thus ( len f) = [\(( len f) / 2)/] & ( len f) = [/(( len f) / 2)\] by A2, INT_1: 25, INT_1: 30;

        f = ( <*> REAL ) by A2;

        hence ( Sum f) = (( Sum f) + ( Sum f)) by RVSUM_1: 72;

        let n;

        f = {} by A2;

        then (f . n) = 0 = (f . (2 * n)) & (f . n) = 0 = (f . ((2 * n) - 1));

        hence thesis;

      end;

      

       A3: P[n] implies P[(n + 1)]

      proof

        assume

         A4: P[n];

        set n1 = (n + 1);

        let f be complex-valued FinSequence such that

         A5: ( len f) = n1;

        set fn = (f | n);

        

         A6: f = (fn ^ <*(f . n1)*>) by A5, FINSEQ_3: 55;

        n < n1 by NAT_1: 13;

        then ( len fn) = n by A5, FINSEQ_1: 59;

        then

        consider e,o be complex-valued FinSequence such that

         A7: ( len e) = [\(n / 2)/] & ( len o) = [/(n / 2)\] and

         A8: ( Sum fn) = (( Sum e) + ( Sum o)) and

         A9: for k holds (e . k) = (fn . (2 * k)) & (o . k) = (fn . ((2 * k) - 1)) by A4;

        per cases ;

          suppose n is even;

          then

          consider k such that

           A10: (2 * k) = n by ABIAN:def 2;

          take e, oF = (o ^ <*(f . n1)*>);

          

           A11: ( len oF) = (( len o) + 1) by FINSEQ_2: 16;

          

           A12: [\(n / 2)/] = k = [\((n + 1) / 2)/] & [/(n / 2)\] = k & [/((n + 1) / 2)\] = (k + 1) by A10, INT_1: 25, INT_1: 30, Lm1, Lm2;

          hence ( len e) = [\(( len f) / 2)/] & ( len oF) = [/(( len f) / 2)\] by FINSEQ_2: 16, A5, A7;

          

          thus ( Sum f) = (( Sum fn) + (f . n1)) by A6, RVSUM_2: 31

          .= (( Sum e) + (( Sum o) + (f . n1))) by A8

          .= (( Sum e) + ( Sum oF)) by RVSUM_2: 31;

          let i be Nat;

          thus (e . i) = (f . (2 * i))

          proof

            per cases ;

              suppose (2 * i) <= n;

              then (fn . (2 * i)) = (f . (2 * i)) by FINSEQ_3: 112;

              hence thesis by A9;

            end;

              suppose (2 * i) > n;

              then

               A13: i > k by A10, XREAL_1: 64;

              then i >= (k + 1) by NAT_1: 13;

              then (2 * i) >= (2 * (k + 1)) & (2 * (k + 1)) = (( len f) + 1) by A10, A5, XREAL_1: 64;

              then (2 * i) > ( len f) by NAT_1: 13;

              then not (2 * i) in ( dom f) & not i in ( dom e) by FINSEQ_3: 25, A7, A12, A13;

              then (f . (2 * i)) = 0 = (e . i) by FUNCT_1:def 2;

              hence thesis;

            end;

          end;

          thus (oF . i) = (f . ((2 * i) - 1))

          proof

            per cases ;

              suppose i = 0 ;

              then not i in ( dom oF) & not ((2 * i) - 1) in ( dom f) by FINSEQ_3: 25;

              then (oF . i) = 0 = (f . ((2 * i) - 1)) by FUNCT_1:def 2;

              hence thesis;

            end;

              suppose

               A14: i <> 0 & (2 * i) <= n;

              then 1 <= i <= k by A10, XREAL_1: 68, NAT_1: 14;

              then i in ( dom o) by A7, A12, FINSEQ_3: 25;

              

              then

               A15: (oF . i) = (o . i) by FINSEQ_1:def 7

              .= (fn . ((2 * i) - 1)) by A9;

              ((2 * i) - 1) <= (n - 0 ) by XREAL_1: 13, A14;

              hence thesis by A15, A14, FINSEQ_3: 112;

            end;

              suppose (2 * i) > n;

              then i > k by A10, XREAL_1: 64;

              then i >= (k + 1) by NAT_1: 13;

              then (2 * i) >= (2 * (k + 1)) & (2 * (k + 1)) = (( len f) + 1) by A10, A5, XREAL_1: 64;

              then

               A16: ((2 * i) - 1) >= ( len f) by XREAL_1: 19;

              per cases by A16, XXREAL_0: 1;

                suppose ((2 * i) - 1) = ( len f);

                hence thesis by A5, A10, A7, A12;

              end;

                suppose

                 A17: ((2 * i) - 1) > ( len f);

                then not ((2 * i) - 1) in ( dom f) by FINSEQ_3: 25;

                then

                 A18: (f . ((2 * i) - 1)) = 0 by FUNCT_1:def 2;

                (2 * i) > (( len f) + 1) by A17, XREAL_1: 20;

                then (2 * i) > (2 * (k + 1)) by A10, A5;

                then i > (k + 1) by XREAL_1: 64;

                then not i in ( dom oF) by A11, A12, A7, FINSEQ_3: 25;

                hence thesis by A18, FUNCT_1:def 2;

              end;

            end;

          end;

        end;

          suppose n is odd;

          then

          consider k such that

           A19: n = ((2 * k) + 1) by ABIAN: 9;

          take eF = (e ^ <*(f . n1)*>), o;

          

           A20: ( len eF) = (( len e) + 1) by FINSEQ_2: 16;

          

           A21: [\(n / 2)/] = k & [\((n + 1) / 2)/] = (k + 1) & [/(n / 2)\] = (k + 1) & [/((n + 1) / 2)\] = (k + 1) by A19, INT_1: 25, INT_1: 30, Lm1, Lm2;

          hence ( len eF) = [\(( len f) / 2)/] & ( len o) = [/(( len f) / 2)\] by FINSEQ_2: 16, A5, A7;

          

          thus ( Sum f) = (( Sum fn) + (f . n1)) by A6, RVSUM_2: 31

          .= ((( Sum e) + (f . n1)) + ( Sum o)) by A8

          .= (( Sum eF) + ( Sum o)) by RVSUM_2: 31;

          let i be Nat;

          thus (eF . i) = (f . (2 * i))

          proof

            per cases ;

              suppose i = 0 ;

              hence thesis;

            end;

              suppose i <> 0 & i <= k;

              then 1 <= i <= k & (2 * i) <= (2 * k) by NAT_1: 14, XREAL_1: 64;

              then i in ( dom e) & (2 * i) < n by A19, NAT_1: 13, FINSEQ_3: 25, A7, A21;

              then (eF . i) = (e . i) & (fn . (2 * i)) = (f . (2 * i)) by FINSEQ_1:def 7, FINSEQ_3: 112;

              hence thesis by A9;

            end;

              suppose i > k;

              then

               A22: i >= (k + 1) by NAT_1: 13;

              per cases by A22, XXREAL_0: 1;

                suppose i = (k + 1);

                hence thesis by A19, A7, A21;

              end;

                suppose

                 A23: i > (k + 1);

                then not i in ( dom eF) by FINSEQ_3: 25, A7, A20, A21;

                then

                 A24: (eF . i) = 0 by FUNCT_1:def 2;

                (2 * i) > (2 * (k + 1)) by A23, XREAL_1: 68;

                then not (2 * i) in ( dom f) by A5, A19, FINSEQ_3: 25;

                hence thesis by A24, FUNCT_1:def 2;

              end;

            end;

          end;

          thus (o . i) = (f . ((2 * i) - 1))

          proof

            per cases ;

              suppose i = 0 ;

              then not i in ( dom o) & not ((2 * i) - 1) in ( dom f) by FINSEQ_3: 25;

              then (o . i) = 0 = (f . ((2 * i) - 1)) by FUNCT_1:def 2;

              hence thesis;

            end;

              suppose

               A25: i <> 0 & ((2 * i) - 1) <= n;

              (fn . ((2 * i) - 1)) = (f . ((2 * i) - 1)) by A25, FINSEQ_3: 112;

              hence thesis by A9;

            end;

              suppose ((2 * i) - 1) > n;

              then (2 * i) > (n + 1) by XREAL_1: 20;

              then (2 * i) > (2 * (k + 1)) by A19;

              then

               A26: i > (k + 1) by XREAL_1: 64;

              then not i in ( dom o) by FINSEQ_3: 25, A7, A21;

              then

               A27: (o . i) = 0 by FUNCT_1:def 2;

              i >= ((k + 1) + 1) by A26, NAT_1: 13;

              then (2 * i) >= (2 * ((k + 1) + 1)) by XREAL_1: 64;

              then (2 * i) >= ((( len f) + 1) + 1) by A19, A5;

              then (2 * i) > (( len f) + 1) by NAT_1: 13;

              then not ((2 * i) - 1) in ( dom f) by XREAL_1: 20, FINSEQ_3: 25;

              hence thesis by A27, FUNCT_1:def 2;

            end;

          end;

        end;

      end;

       P[n] from NAT_1:sch 2( A1, A3);

      hence thesis;

    end;

    registration

      let a;

      cluster ((a ^2 ) -' 1) -> non square;

      coherence

      proof

        assume

         A1: ((a ^2 ) -' 1) is square;

        a >= 2 by NAT_2: 29;

        then

         A2: (a ^2 ) >= (2 * 2) by XREAL_1: 66;

        

         A3: ((a ^2 ) -' 1) = ((a ^2 ) - 1) by XREAL_1: 233, NAT_1: 14;

        then ((a ^2 ) -' 1) is non zero by A2;

        then (((a ^2 ) -' 1) + 1) is non square by A1;

        hence thesis by A3;

      end;

    end

    begin

    definition

      let a,n be Nat;

      assume

       A1: a is non trivial;

      :: HILB10_1:def1

      func Px (a,n) -> Nat means

      : Def1: for b be non trivial Nat st b = a holds ex y be Nat st (it + (y * ( sqrt ((b ^2 ) -' 1)))) = (((( min_Pell's_solution_of ((b ^2 ) -' 1)) `1 ) + ((( min_Pell's_solution_of ((b ^2 ) -' 1)) `2 ) * ( sqrt ((b ^2 ) -' 1)))) |^ n);

      existence

      proof

        reconsider A = a as non trivial Nat by A1;

        consider x,y be Nat such that

         A2: (x + (y * ( sqrt ((A ^2 ) -' 1)))) = (((( min_Pell's_solution_of ((A ^2 ) -' 1)) `1 ) + ((( min_Pell's_solution_of ((A ^2 ) -' 1)) `2 ) * ( sqrt ((A ^2 ) -' 1)))) |^ n) by PELLS_EQ: 4;

        take x;

        thus thesis by A2;

      end;

      uniqueness

      proof

        reconsider A = a as non trivial Nat by A1;

        let p1,p2 be Nat such that

         A3: for b be non trivial Nat st b = a holds ex y be Nat st (p1 + (y * ( sqrt ((b ^2 ) -' 1)))) = (((( min_Pell's_solution_of ((b ^2 ) -' 1)) `1 ) + ((( min_Pell's_solution_of ((b ^2 ) -' 1)) `2 ) * ( sqrt ((b ^2 ) -' 1)))) |^ n) and

         A4: for b be non trivial Nat st b = a holds ex y be Nat st (p2 + (y * ( sqrt ((b ^2 ) -' 1)))) = (((( min_Pell's_solution_of ((b ^2 ) -' 1)) `1 ) + ((( min_Pell's_solution_of ((b ^2 ) -' 1)) `2 ) * ( sqrt ((b ^2 ) -' 1)))) |^ n);

        set m = ( min_Pell's_solution_of ((A ^2 ) -' 1));

        

         A5: ex y be Nat st (p1 + (y * ( sqrt ((A ^2 ) -' 1)))) = (((m `1 ) + ((m `2 ) * ( sqrt ((A ^2 ) -' 1)))) |^ n) by A3;

        ex y be Nat st (p2 + (y * ( sqrt ((A ^2 ) -' 1)))) = (((m `1 ) + ((m `2 ) * ( sqrt ((A ^2 ) -' 1)))) |^ n) by A4;

        hence thesis by A5, PELLS_EQ: 3;

      end;

    end

    definition

      let a,n be Nat;

      assume

       A1: a is non trivial;

      :: HILB10_1:def2

      func Py (a,n) -> Nat means

      : Def2: for b be non trivial Nat st b = a holds (( Px (b,n)) + (it * ( sqrt ((b ^2 ) -' 1)))) = (((( min_Pell's_solution_of ((b ^2 ) -' 1)) `1 ) + ((( min_Pell's_solution_of ((b ^2 ) -' 1)) `2 ) * ( sqrt ((b ^2 ) -' 1)))) |^ n);

      existence

      proof

        reconsider A = a as non trivial Nat by A1;

        consider y be Nat such that

         A2: (( Px (A,n)) + (y * ( sqrt ((A ^2 ) -' 1)))) = (((( min_Pell's_solution_of ((A ^2 ) -' 1)) `1 ) + ((( min_Pell's_solution_of ((A ^2 ) -' 1)) `2 ) * ( sqrt ((A ^2 ) -' 1)))) |^ n) by Def1;

        take y;

        thus thesis by A2;

      end;

      uniqueness

      proof

        reconsider A = a as non trivial Nat by A1;

        let p1,p2 be Nat such that

         A3: for b be non trivial Nat st b = a holds (( Px (b,n)) + (p1 * ( sqrt ((b ^2 ) -' 1)))) = (((( min_Pell's_solution_of ((b ^2 ) -' 1)) `1 ) + ((( min_Pell's_solution_of ((b ^2 ) -' 1)) `2 ) * ( sqrt ((b ^2 ) -' 1)))) |^ n) and

         A4: for b be non trivial Nat st b = a holds (( Px (b,n)) + (p2 * ( sqrt ((b ^2 ) -' 1)))) = (((( min_Pell's_solution_of ((b ^2 ) -' 1)) `1 ) + ((( min_Pell's_solution_of ((b ^2 ) -' 1)) `2 ) * ( sqrt ((b ^2 ) -' 1)))) |^ n);

        set m = ( min_Pell's_solution_of ((A ^2 ) -' 1));

        (( Px (A,n)) + (p1 * ( sqrt ((A ^2 ) -' 1)))) = (((m `1 ) + ((m `2 ) * ( sqrt ((A ^2 ) -' 1)))) |^ n) = (( Px (A,n)) + (p2 * ( sqrt ((A ^2 ) -' 1)))) by A3, A4;

        hence thesis by PELLS_EQ: 3;

      end;

    end

    theorem :: HILB10_1:3

    

     Th6: ( Px (a, 0 )) = 1 & ( Py (a, 0 )) = 0

    proof

      set A = ((a ^2 ) -' 1), M = ( min_Pell's_solution_of A);

      (( Px (a, 0 )) + (( Py (a, 0 )) * ( sqrt ((a ^2 ) -' 1)))) = (((M `1 ) + ((M `2 ) * ( sqrt A))) |^ 0 ) by Def2

      .= (1 + ( 0 * ( sqrt A))) by NEWTON: 4;

      hence thesis by PELLS_EQ: 3;

    end;

    

     Lm3: for x,y be Integer, D be Nat holds ((x ^2 ) - (D * (y ^2 ))) = 1 iff [x, y] is Pell's_solution of D

    proof

      let x,y be Integer, D be Nat;

      

       A1: ( [x, y] `1 ) = x & ( [x, y] `2 ) = y;

      x in INT & y in INT by INT_1:def 2;

      then [x, y] in [: INT , INT :] by ZFMISC_1: 87;

      hence ((x ^2 ) - (D * (y ^2 ))) = 1 implies [x, y] is Pell's_solution of D by A1, PELLS_EQ:def 1;

      assume [x, y] is Pell's_solution of D;

      hence thesis by PELLS_EQ:def 1, A1;

    end;

    theorem :: HILB10_1:4

    

     Th7: [n1, n2] is Pell's_solution of ((a ^2 ) -' 1) implies ex n st n1 = ( Px (a,n)) & n2 = ( Py (a,n))

    proof

      set D = ((a ^2 ) -' 1);

      assume

       A1: [n1, n2] is Pell's_solution of D;

      then

      reconsider N = [n1, n2] as Pell's_solution of D;

      

       A2: ((n1 ^2 ) - (((a ^2 ) -' 1) * (n2 ^2 ))) = 1 by A1, Lm3;

      per cases ;

        suppose

         A3: n2 = 0 ;

        then n1 <= 1 & n1 >= 1 by A2, SQUARE_1: 51, NAT_1: 14;

        then n1 = 1 by XXREAL_0: 1;

        then n1 = ( Px (a, 0 )) & n2 = ( Py (a, 0 )) by A3, Th6;

        hence thesis;

      end;

        suppose n2 > 0 ;

        then N is positive by A2;

        then

        consider n be positive Nat such that

         A4: (n1 + (n2 * ( sqrt D))) = (((( min_Pell's_solution_of D) `1 ) + ((( min_Pell's_solution_of D) `2 ) * ( sqrt D))) |^ n) by PELLS_EQ: 21;

        consider y be Nat such that

         A5: (( Px (a,n)) + (y * ( sqrt D))) = (((( min_Pell's_solution_of D) `1 ) + ((( min_Pell's_solution_of D) `2 ) * ( sqrt D))) |^ n) by Def1;

        

         A6: n1 = ( Px (a,n)) by A5, A4, PELLS_EQ: 3;

        (( Px (a,n)) + (( Py (a,n)) * ( sqrt D))) = (n1 + (n2 * ( sqrt D))) by A4, Def2;

        then n2 = ( Py (a,n)) by PELLS_EQ: 3;

        hence thesis by A6;

      end;

    end;

    theorem :: HILB10_1:5

    

     Th8: [a, 1] = ( min_Pell's_solution_of ((a ^2 ) -' 1))

    proof

      set A = ((a ^2 ) -' 1), M = ( min_Pell's_solution_of A);

      assume

       A1: [a, 1] <> M;

      ((a ^2 ) -' 1) = ((a ^2 ) - 1) by XREAL_1: 233, NAT_1: 14;

      then ((a ^2 ) - (((a ^2 ) -' 1) * (1 ^2 ))) = 1;

      then

      reconsider a1 = [a, 1] as Pell's_solution of A by Lm3;

      (M `1 ) <> a or (M `2 ) <> 1 by A1;

      then

       A2: ((M `1 ) + ((M `2 ) * ( sqrt A))) <> (a + (1 * ( sqrt A))) by PELLS_EQ: 3;

      

       A3: ( sqrt A) >= 0 by SQUARE_1:def 2;

      a1 is positive;

      then

       A4: (M `1 ) <= (a1 `1 ) & (M `2 ) <= (a1 `2 ) by PELLS_EQ:def 3;

      then ((M `2 ) * ( sqrt A)) <= ((a1 `2 ) * ( sqrt A)) by A3, XREAL_1: 64;

      then ((M `1 ) + ((M `2 ) * ( sqrt A))) <= ((a1 `1 ) + ((a1 `2 ) * ( sqrt A))) by A4, XREAL_1: 7;

      then

       A5: ((M `1 ) + ((M `2 ) * ( sqrt A))) < ((a1 `1 ) + ((a1 `2 ) * ( sqrt A))) by A2, XXREAL_0: 1;

      1 < ((M `1 ) + ((M `2 ) * ( sqrt A))) by PELLS_EQ: 18;

      hence thesis by NAT_1: 14, A5, PELLS_EQ: 19;

    end;

    theorem :: HILB10_1:6

    

     Th9: ( Px (a,(n + 1))) = ((( Px (a,n)) * a) + (( Py (a,n)) * ((a ^2 ) -' 1))) & ( Py (a,(n + 1))) = (( Px (a,n)) + (( Py (a,n)) * a))

    proof

      set A = ((a ^2 ) -' 1), M = ( min_Pell's_solution_of A);

      set n1 = (n + 1);

      

       A1: (( sqrt A) ^2 ) = A by SQUARE_1:def 2;

      

       A2: M = [a, 1] by Th8;

      (( Px (a,n1)) + (( Py (a,n1)) * ( sqrt A))) = (((M `1 ) + ((M `2 ) * ( sqrt A))) |^ n1) by Def2

      .= ((((M `1 ) + ((M `2 ) * ( sqrt A))) |^ n) * ((M `1 ) + ((M `2 ) * ( sqrt A)))) by NEWTON: 6

      .= ((( Px (a,n)) + (( Py (a,n)) * ( sqrt A))) * ((M `1 ) + ((M `2 ) * ( sqrt A)))) by Def2

      .= (((( Px (a,n)) * a) + (( Py (a,n)) * A)) + ((( Px (a,n)) + (( Py (a,n)) * a)) * ( sqrt A))) by A2, A1;

      hence thesis by PELLS_EQ: 3;

    end;

    theorem :: HILB10_1:7

    

     Th10: ((( Px (a,n)) ^2 ) - (((a ^2 ) -' 1) * (( Py (a,n)) ^2 ))) = 1

    proof

      set m = ( min_Pell's_solution_of ((a ^2 ) -' 1));

      per cases ;

        suppose n = 0 ;

        then ( Px (a,n)) = 1 & ( Py (a,n)) = 0 by Th6;

        hence thesis;

      end;

        suppose

         A1: n > 0 ;

        (( Px (a,n)) + (( Py (a,n)) * ( sqrt ((a ^2 ) -' 1)))) = (((m `1 ) + ((m `2 ) * ( sqrt ((a ^2 ) -' 1)))) |^ n) by Def2;

        then

        reconsider PP = [( Px (a,n)), ( Py (a,n))] as positive Pell's_solution of ((a ^2 ) -' 1) by A1, PELLS_EQ: 20;

        (((PP `1 ) ^2 ) - (((a ^2 ) -' 1) * ((PP `2 ) ^2 ))) = 1 by PELLS_EQ:def 1;

        hence thesis;

      end;

    end;

    theorem :: HILB10_1:8

    

     Th11: (( Px (a,n)) + (( Py (a,n)) * ( sqrt ((a ^2 ) -' 1)))) = ((a + ( sqrt ((a ^2 ) -' 1))) |^ n) & (( Px (a,n)) + (( - ( Py (a,n))) * ( sqrt ((a ^2 ) -' 1)))) = ((a - ( sqrt ((a ^2 ) -' 1))) |^ n)

    proof

      set A = ((a ^2 ) -' 1), M = ( min_Pell's_solution_of A);

      set n1 = (n + 1);

      

       A1: M = [a, 1] by Th8;

      

       A2: (( Px (a,n)) + (( Py (a,n)) * ( sqrt A))) = (((M `1 ) + ((M `2 ) * ( sqrt A))) |^ n) by Def2

      .= ((a + (1 * ( sqrt A))) |^ n) by A1;

      then (( Px (a,n)) - (( Py (a,n)) * ( sqrt A))) = ((a - (1 * ( sqrt A))) |^ n) by PELLS_EQ: 6;

      hence thesis by A2;

    end;

    theorem :: HILB10_1:9

    

     Th12: ex Fy,Fx be FinSequence of NAT st ( Sum Fy) = ( Py (a,n)) & ( len Fy) = [\((n + 1) / 2)/] & (for i st 1 <= i <= ((n + 1) / 2) holds (Fy . i) = (((n choose ((2 * i) -' 1)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2 ) -' 1) |^ (i -' 1)))) & ((a |^ n) + ( Sum Fx)) = ( Px (a,n)) & ( len Fx) = [\(n / 2)/] & for i st 1 <= i <= (n / 2) holds (Fx . i) = (((n choose (2 * i)) * (a |^ (n -' (2 * i)))) * (((a ^2 ) -' 1) |^ i))

    proof

      set A = ((a ^2 ) -' 1);

      defpred P[ Nat] means ex Fy,Fx be FinSequence of NAT st ( Sum Fy) = ( Py (a,$1)) & ( len Fy) = [\(($1 + 1) / 2)/] & (for i be Nat st 1 <= i <= (($1 + 1) / 2) holds (Fy . i) = ((($1 choose ((2 * i) -' 1)) * (a |^ (($1 + 1) -' (2 * i)))) * (A |^ (i -' 1)))) & ((a |^ $1) + ( Sum Fx)) = ( Px (a,$1)) & ( len Fx) = [\($1 / 2)/] & for i be Nat st 1 <= i <= ($1 / 2) holds (Fx . i) = ((($1 choose (2 * i)) * (a |^ ($1 -' (2 * i)))) * (A |^ i));

      

       A1: P[ 0 ]

      proof

        set F = ( <*> NAT );

        

         A2: ( len F) = 0 ;

        

         A3: 0 = [\((( 0 * 2) + 1) / 2)/] by Lm1;

        

         A4: for i be Nat st 1 <= i <= (( 0 + 1) / 2) holds (F . i) = ((( 0 choose ((2 * i) -' 1)) * (a |^ (( 0 + 1) -' (2 * i)))) * (A |^ (i -' 1))) by XXREAL_0: 2;

        

         A5: ( Sum F) = ( Py (a, 0 )) by Th6, RVSUM_1: 72;

        (a |^ 0 ) = 1 by NEWTON: 4;

        then

         A6: ((a |^ 0 ) + ( Sum F)) = ( Px (a, 0 )) by RVSUM_1: 72, Th6;

        for i be Nat st 1 <= i <= ( 0 / 2) holds (F . i) = ((( 0 choose (2 * i)) * (a |^ ( 0 -' (2 * i)))) * (A |^ i));

        hence thesis by A2, A3, A4, A5, A6;

      end;

      

       A7: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n;

        set n1 = (n + 1);

        assume P[n];

        then

        consider Fy,Fx be FinSequence of NAT such that

         A8: ( Sum Fy) = ( Py (a,n)) & ( len Fy) = [\(n1 / 2)/] and

         A9: for i be Nat st 1 <= i <= (n1 / 2) holds (Fy . i) = (((n choose ((2 * i) -' 1)) * (a |^ (n1 -' (2 * i)))) * (A |^ (i -' 1))) and

         A10: ((a |^ n) + ( Sum Fx)) = ( Px (a,n)) & ( len Fx) = [\(n / 2)/] and

         A11: for i be Nat st 1 <= i <= (n / 2) holds (Fx . i) = (((n choose (2 * i)) * (a |^ (n -' (2 * i)))) * (A |^ i));

        set Fxa = ( <*(a |^ n)*> ^ Fx);

        set Fx0 = (Fx ^ <* 0 *>);

        set Fy0 = (Fy ^ <* 0 *>);

        

         A12: ( Px (a,n1)) = ((((a |^ n) + ( Sum Fx)) * a) + (( Sum Fy) * A)) by Th9, A8, A10

        .= ((((a |^ n) * a) + (( Sum Fx) * a)) + (( Sum Fy) * A))

        .= (((a |^ n1) + (( Sum Fx) * a)) + (( Sum Fy) * A)) by NEWTON: 6

        .= (((a |^ n1) + ( Sum (a * Fx))) + (( Sum Fy) * A)) by RVSUM_1: 87;

        

         A13: (( Sum Fy) * A) = ( Sum (A * Fy)) by RVSUM_1: 87;

        

         A14: ( Sum Fy0) = (( Sum Fy) + 0 ) by RVSUM_1: 74;

        

         A15: ( Sum Fx0) = (( Sum Fx) + 0 ) by RVSUM_1: 74;

        

         A16: ( Sum (a * Fx0)) = (a * ( Sum Fx0)) by RVSUM_1: 87;

        

         A17: ( Py (a,n1)) = (( Px (a,n)) + (( Py (a,n)) * a)) by Th9

        .= (( Sum Fxa) + (( Sum Fy) * a)) by A8, A10, RVSUM_1: 76;

        per cases ;

          suppose

           A18: n is odd;

          then

          consider k such that

           A19: n = ((2 * k) + 1) by ABIAN: 9;

          set k1 = (k + 1);

          

           A20: [\(n1 / 2)/] = k1 & [\(n / 2)/] = k by A19, INT_1: 25, Lm1;

          then

           A21: ( len Fxa) = k1 & ( len (a * Fy)) = k1 by A10, FINSEQ_5: 8, A8, RVSUM_1: 117;

          ( rng Fxa) c= REAL & ( rng (a * Fy)) c= REAL ;

          then Fxa is FinSequence of REAL & (a * Fy) is FinSequence of REAL by FINSEQ_1:def 4;

          then

          reconsider FxA = Fxa, aFy = (a * Fy) as Element of (k1 -tuples_on REAL ) by A21, FINSEQ_2: 92;

          ( rng (Fxa + (a * Fy))) c= NAT by VALUED_0:def 6;

          then

          reconsider FY = (Fxa + (a * Fy)) as FinSequence of NAT by FINSEQ_1:def 4;

          

           A22: ( len (a * Fx0)) = ( len Fx0) = k1 & ( len (A * Fy)) = k1 by A20, A8, A10, FINSEQ_2: 16, RVSUM_1: 117;

          reconsider AFx0 = (a * Fx0), AFy = (A * Fy) as Element of (k1 -tuples_on REAL ) by A22, FINSEQ_2: 92;

          ( rng ((a * Fx0) + (A * Fy))) c= NAT by VALUED_0:def 6;

          then

          reconsider FX = ((a * Fx0) + (A * Fy)) as FinSequence of NAT by FINSEQ_1:def 4;

          take FY, FX;

          

          thus ( Sum FY) = (( Sum FxA) + ( Sum aFy)) by RVSUM_1: 89

          .= ( Py (a,n1)) by A17, RVSUM_1: 87;

          

           A23: (n1 + 1) = ((2 * k1) + 1) by A19;

          ( len (FxA + aFy)) = k1 by CARD_1:def 7;

          hence ( len FY) = [\((n1 + 1) / 2)/] by A23, Lm1;

          thus for i be Nat st 1 <= i <= ((n1 + 1) / 2) holds (FY . i) = (((n1 choose ((2 * i) -' 1)) * (a |^ ((n1 + 1) -' (2 * i)))) * (A |^ (i -' 1)))

          proof

            let i be Nat such that

             A24: 1 <= i <= ((n1 + 1) / 2);

            set i1 = (i -' 1);

            

             A25: (i1 + 1) = i by A24, XREAL_1: 235;

            (2 * 1) <= (2 * i) by A24, XREAL_1: 66;

            then

             A26: ((2 * i) -' 1) = ((2 * i) - 1) by XREAL_1: 233, XXREAL_0: 2;

            

             A27: (2 * i) <= (n1 + 1) by A24, XREAL_1: 83;

            then

             A28: (2 * i) < (n1 + 1) by A18, XXREAL_0: 1;

            then

             A29: (2 * i) <= n1 by NAT_1: 13;

            

             A30: i <= (n1 / 2) by A28, NAT_1: 13, XREAL_1: 77;

            

             A31: (n1 -' (2 * i)) = (n1 - (2 * i)) by A29, XREAL_1: 233;

            

             A32: ((n1 + 1) -' (2 * i)) = ((n1 + 1) - (2 * i)) by XREAL_1: 233, A27;

            then

             A33: ((n1 + 1) -' (2 * i)) = (1 + (n1 -' (2 * i))) by A31;

            (Fy . i) = (((n choose ((2 * i) -' 1)) * (a |^ (n1 -' (2 * i)))) * (A |^ i1)) by A24, A9, A30;

            

            then

             A34: ((a * Fy) . i) = (a * (((n choose ((2 * i) -' 1)) * (a |^ (n1 -' (2 * i)))) * (A |^ i1))) by VALUED_1: 6

            .= (((n choose ((2 * i) -' 1)) * (a * (a |^ (n1 -' (2 * i))))) * (A |^ i1))

            .= (((n choose ((2 * i1) + 1)) * (a |^ ((n1 + 1) -' (2 * i)))) * (A |^ i1)) by A26, A25, A33, NEWTON: 6;

            (2 * i) <= (n1 + 1) by A24, XREAL_1: 83;

            then (((2 * i1) + 1) + 1) <= (n1 + 1) by A25;

            then ((2 * i1) + 1) <= n1 by XREAL_1: 8;

            then

             A35: (2 * i1) < n1 by NAT_1: 13;

            then

             A36: (2 * i1) <= n by NAT_1: 13;

            then

             A37: (n -' (2 * i1)) = (n - (2 * i1)) by XREAL_1: 233;

            

             A38: (Fxa . i) = (((n choose (2 * i1)) * (a |^ (n -' (2 * i1)))) * (A |^ i1))

            proof

              per cases ;

                suppose

                 A39: i > 1;

                then

                 A40: i1 >= 1 by A25, NAT_1: 13;

                i1 <= (n / 2) by XREAL_1: 77, A35, NAT_1: 13;

                then

                 A41: (Fx . i1) = (((n choose (2 * i1)) * (a |^ (n -' (2 * i1)))) * (A |^ i1)) by A11, A39, A25, NAT_1: 13;

                (2 * i1) < ((2 * k) + 1) by A36, A19, XXREAL_0: 1;

                then i1 <= k by XREAL_1: 68, NAT_1: 13;

                then i1 in ( dom Fx) by A40, A20, A10, FINSEQ_3: 25;

                hence thesis by A41, A25, FINSEQ_3: 103;

              end;

                suppose i <= 1;

                then

                 A42: i = 1 by A24, XXREAL_0: 1;

                

                 A43: (n choose (2 * i1)) = 1 by A42, A25, NEWTON: 19;

                (n -' (2 * i1)) = (n - 0 ) by A42, A25, XREAL_1: 233;

                hence thesis by A43, NEWTON: 4, A42, A25;

              end;

            end;

            

            thus (FY . i) = ((FxA . i) + (aFy . i)) by RVSUM_1: 11

            .= ((((n choose (2 * i1)) + (n choose ((2 * i1) + 1))) * (a |^ ((n1 + 1) -' (2 * i)))) * (A |^ i1)) by A38, A34, A37, A32, A25

            .= (((n1 choose ((2 * i) -' 1)) * (a |^ ((n1 + 1) -' (2 * i)))) * (A |^ i1)) by A26, A25, NEWTON: 22;

          end;

          ( Sum FX) = (( Sum AFx0) + ( Sum AFy)) by RVSUM_1: 89

          .= (( Sum (a * Fx)) + ( Sum (A * Fy))) by RVSUM_1: 87, A15, A16;

          hence ((a |^ n1) + ( Sum FX)) = ( Px (a,n1)) by A12, A13;

          ( len (AFx0 + AFy)) = k1 by CARD_1:def 7;

          hence ( len FX) = [\(n1 / 2)/] by A19, INT_1: 25;

          thus for i be Nat st 1 <= i <= (n1 / 2) holds (FX . i) = (((n1 choose (2 * i)) * (a |^ (n1 -' (2 * i)))) * (A |^ i))

          proof

            let i be Nat such that

             A44: 1 <= i <= (n1 / 2);

            set i1 = (i -' 1);

            (i1 + 1) = i by A44, XREAL_1: 235;

            then

             A45: (A * (A |^ i1)) = (A |^ i) by NEWTON: 6;

            (Fy . i) = (((n choose ((2 * i) -' 1)) * (a |^ (n1 -' (2 * i)))) * (A |^ i1)) by A9, A44;

            

            then

             A46: ((A * Fy) . i) = (A * (((n choose ((2 * i) -' 1)) * (a |^ (n1 -' (2 * i)))) * (A |^ i1))) by VALUED_1: 6

            .= (((n choose ((2 * i) -' 1)) * (a |^ (n1 -' (2 * i)))) * (A |^ i)) by A45;

            (2 * i) <= n1 by A44, XREAL_1: 83;

            then

             A47: (n1 -' (2 * i)) = (n1 - (2 * i)) by XREAL_1: 233;

            

             A48: ((a * Fx0) . i) = (a * (Fx0 . i)) by VALUED_1: 6;

            

             A49: ((a * Fx0) . i) = (((n choose (2 * i)) * (a |^ (n1 -' (2 * i)))) * (A |^ i))

            proof

              per cases ;

                suppose

                 A50: i <= k;

                then

                 A51: (2 * i) < n by A19, NAT_1: 13, XREAL_1: 66;

                then i <= (n / 2) by XREAL_1: 77;

                then

                 A52: (Fx . i) = (((n choose (2 * i)) * (a |^ (n -' (2 * i)))) * (A |^ i)) by A11, A44;

                

                 A53: i in ( dom Fx) by A44, A50, A10, A20, FINSEQ_3: 25;

                

                 A54: (n -' (2 * i)) = (n - (2 * i)) by A51, XREAL_1: 233;

                (n1 -' (2 * i)) = (1 + (n -' (2 * i))) by A54, A47;

                then

                 A55: (a |^ (n1 -' (2 * i))) = (a * (a |^ (n -' (2 * i)))) by NEWTON: 6;

                ((a * Fx0) . i) = (a * (((n choose (2 * i)) * (a |^ (n -' (2 * i)))) * (A |^ i))) by A48, A52, A53, FINSEQ_1:def 7

                .= (((n choose (2 * i)) * (a |^ (n1 -' (2 * i)))) * (A |^ i)) by A55;

                hence thesis;

              end;

                suppose i > k;

                then i >= k1 by NAT_1: 13;

                then

                 A56: (2 * i) >= (2 * k1) by XREAL_1: 66;

                then

                 A57: (2 * i) >= n1 by A19;

                (2 * i) <= n1 by A44, XREAL_1: 83;

                then

                 A58: (2 * i) = (2 * k1) by A56, A19, XXREAL_0: 1;

                (2 * i) > n by A57, NAT_1: 13;

                then (n choose (2 * i)) = 0 by NEWTON:def 3;

                hence thesis by A58, A10, A20, A48;

              end;

            end;

            

             A59: (((2 * i) -' 1) + 1) = (2 * i) by XREAL_1: 235, NAT_1: 14, A44;

            

            thus (FX . i) = ((AFx0 . i) + (AFy . i)) by RVSUM_1: 11

            .= ((((n choose ((2 * i) -' 1)) + (n choose (2 * i))) * (a |^ (n1 -' (2 * i)))) * (A |^ i)) by A46, A49

            .= (((n1 choose (2 * i)) * (a |^ (n1 -' (2 * i)))) * (A |^ i)) by A59, NEWTON: 22;

          end;

        end;

          suppose n is even;

          then

          consider k such that

           A60: n = (2 * k) by ABIAN:def 2;

          set k1 = (k + 1);

          

           A61: [\(n1 / 2)/] = k & [\(n / 2)/] = k by A60, INT_1: 25, Lm1;

          then

           A62: ( len Fxa) = k1 & ( len Fy0) = k1 & ( len (a * Fy0)) = ( len Fy0) by FINSEQ_2: 16, FINSEQ_5: 8, A8, A10, RVSUM_1: 117;

          ( rng Fxa) c= REAL & ( rng (a * Fy0)) c= REAL ;

          then Fxa is FinSequence of REAL & (a * Fy0) is FinSequence of REAL by FINSEQ_1:def 4;

          then

          reconsider FxA = Fxa, aFy0 = (a * Fy0) as Element of (k1 -tuples_on REAL ) by A62, FINSEQ_2: 92;

          ( rng (Fxa + (a * Fy0))) c= NAT by VALUED_0:def 6;

          then

          reconsider FY = (Fxa + (a * Fy0)) as FinSequence of NAT by FINSEQ_1:def 4;

          

           A63: ( len (a * Fx)) = ( len Fx) = k & ( len (A * Fy)) = k by A61, A8, A10, RVSUM_1: 117;

          reconsider AFx = (a * Fx), AFy = (A * Fy) as Element of (k -tuples_on REAL ) by A63, FINSEQ_2: 92;

          ( rng ((a * Fx) + (A * Fy))) c= NAT by VALUED_0:def 6;

          then

          reconsider FX = ((a * Fx) + (A * Fy)) as FinSequence of NAT by FINSEQ_1:def 4;

          take FY, FX;

          

          thus ( Sum FY) = (( Sum FxA) + ( Sum aFy0)) by RVSUM_1: 89

          .= ( Py (a,n1)) by A17, A14, RVSUM_1: 87;

          ( len (FxA + aFy0)) = k1 by CARD_1:def 7;

          hence ( len FY) = [\((n1 + 1) / 2)/] by A60, INT_1: 25;

          thus for i be Nat st 1 <= i <= ((n1 + 1) / 2) holds (FY . i) = (((n1 choose ((2 * i) -' 1)) * (a |^ ((n1 + 1) -' (2 * i)))) * (A |^ (i -' 1)))

          proof

            let i be Nat such that

             A64: 1 <= i <= ((n1 + 1) / 2);

            set i1 = (i -' 1);

            

             A65: (i1 + 1) = i by A64, XREAL_1: 235;

            

             A66: (2 * i) <= (n1 + 1) by A64, XREAL_1: 83;

            then

             A67: ((2 * i1) + 2) <= (n + 2) by A65;

            then

             A68: (2 * i1) <= n by XREAL_1: 8;

            

             A69: (n -' (2 * i1)) = (n - (2 * i1)) & ((n1 + 1) -' (2 * i)) = ((n1 + 1) - (2 * i)) by A67, A66, XREAL_1: 8, XREAL_1: 233;

            (2 * 1) <= (2 * i) by A64, XREAL_1: 66;

            then

             A70: ((2 * i) -' 1) = ((2 * i) - 1) by XREAL_1: 233, XXREAL_0: 2;

            

             A71: (FxA . i) = (((n choose (2 * i1)) * (a |^ ((n1 + 1) -' (2 * i)))) * (A |^ i1))

            proof

              per cases ;

                suppose

                 A72: i > 1;

                then

                 A73: i1 >= 1 by A65, NAT_1: 13;

                i1 <= (n / 2) by A68, XREAL_1: 77;

                then

                 A74: (Fx . i1) = (((n choose (2 * i1)) * (a |^ (n -' (2 * i1)))) * (A |^ i1)) by A11, A72, A65, NAT_1: 13;

                i1 <= k by A68, A60, XREAL_1: 68;

                then i1 in ( dom Fx) by A73, A61, A10, FINSEQ_3: 25;

                hence thesis by A69, A74, A65, FINSEQ_3: 103;

              end;

                suppose i <= 1;

                then

                 A75: i = 1 by A64, XXREAL_0: 1;

                

                 A76: (n choose (2 * i1)) = 1 by A75, A65, NEWTON: 19;

                ((n1 + 1) -' (2 * i)) = ((n + 2) - (2 * 1)) by A75, NAT_1: 11, XREAL_1: 233;

                hence thesis by A76, NEWTON: 4, A75, A65;

              end;

            end;

            

             A77: ((a * Fy0) . i) = (((n choose ((2 * i1) + 1)) * (a |^ ((n1 + 1) -' (2 * i)))) * (A |^ i1))

            proof

              per cases ;

                suppose

                 A78: i <= k;

                then

                 A79: (2 * i) <= n1 by NAT_1: 13, A60, XREAL_1: 66;

                then

                 A80: (2 * i) <= (n1 + 1) by NAT_1: 13;

                i <= (n1 / 2) by A79, XREAL_1: 77;

                then

                 A81: (Fy . i) = (((n choose ((2 * i) -' 1)) * (a |^ (n1 -' (2 * i)))) * (A |^ i1)) by A9, A64;

                i in ( dom Fy) by A64, A78, A8, A61, FINSEQ_3: 25;

                then

                 A82: (Fy . i) = (Fy0 . i) by FINSEQ_1:def 7;

                

                 A83: (n1 -' (2 * i)) = (n1 - (2 * i)) & ((n1 + 1) -' (2 * i)) = ((n1 + 1) - (2 * i)) by A79, A80, XREAL_1: 233;

                ((n1 + 1) -' (2 * i)) = (1 + (n1 -' (2 * i))) by A83;

                then

                 A84: (a |^ ((n1 + 1) -' (2 * i))) = (a * (a |^ (n1 -' (2 * i)))) by NEWTON: 6;

                ((a * Fy0) . i) = (a * (((n choose ((2 * i) -' 1)) * (a |^ (n1 -' (2 * i)))) * (A |^ i1))) by A81, A82, VALUED_1: 6

                .= (((n choose ((2 * i) -' 1)) * (a |^ ((n1 + 1) -' (2 * i)))) * (A |^ i1)) by A84;

                hence thesis by A70, A65;

              end;

                suppose

                 A85: i > k;

                then i1 >= k by A65, NAT_1: 13;

                then

                 A86: ((2 * i1) + 1) > n by NAT_1: 13, A60, XREAL_1: 66;

                i >= k1 by A85, NAT_1: 13;

                then (2 * i) >= (2 * k1) by XREAL_1: 66;

                then (2 * i) = (2 * k1) by A60, A66, XXREAL_0: 1;

                then (Fy0 . i) = 0 by A8, A61;

                then

                 A87: ((a * Fy0) . i) = (a * 0 ) by VALUED_1: 6;

                (n choose ((2 * i1) + 1)) = 0 by A86, NEWTON:def 3;

                hence thesis by A87;

              end;

            end;

            

            thus (FY . i) = ((FxA . i) + (aFy0 . i)) by RVSUM_1: 11

            .= ((((n choose (2 * i1)) + (n choose ((2 * i1) + 1))) * (a |^ ((n1 + 1) -' (2 * i)))) * (A |^ i1)) by A71, A77

            .= (((n1 choose ((2 * i) -' 1)) * (a |^ ((n1 + 1) -' (2 * i)))) * (A |^ i1)) by A70, A65, NEWTON: 22;

          end;

          ( Sum FX) = (( Sum AFx) + ( Sum AFy)) by RVSUM_1: 89

          .= (( Sum (a * Fx)) + ( Sum (A * Fy)));

          hence ((a |^ n1) + ( Sum FX)) = ( Px (a,n1)) by A12, A13;

          ( len (AFx + AFy)) = k by CARD_1:def 7;

          hence ( len FX) = [\(n1 / 2)/] by A60, Lm1;

          thus for i be Nat st 1 <= i <= (n1 / 2) holds (FX . i) = (((n1 choose (2 * i)) * (a |^ (n1 -' (2 * i)))) * (A |^ i))

          proof

            let i be Nat such that

             A88: 1 <= i <= (n1 / 2);

            set i1 = (i -' 1);

            (i1 + 1) = i by A88, XREAL_1: 235;

            then

             A89: (A * (A |^ i1)) = (A |^ i) by NEWTON: 6;

            (Fy . i) = (((n choose ((2 * i) -' 1)) * (a |^ (n1 -' (2 * i)))) * (A |^ i1)) by A9, A88;

            

            then

             A90: ((A * Fy) . i) = (A * (((n choose ((2 * i) -' 1)) * (a |^ (n1 -' (2 * i)))) * (A |^ i1))) by VALUED_1: 6

            .= (((n choose ((2 * i) -' 1)) * (a |^ (n1 -' (2 * i)))) * (A |^ i)) by A89;

            

             A91: (2 * i) <= n1 by A88, XREAL_1: 83;

            then

             A92: (n1 -' (2 * i)) = (n1 - (2 * i)) by XREAL_1: 233;

            

             A93: (2 * i) < n1 by A91, A60, XXREAL_0: 1;

            then

             A94: (2 * i) <= n by NAT_1: 13;

            

             A95: i <= (n / 2) by A93, NAT_1: 13, XREAL_1: 77;

            

             A96: (n -' (2 * i)) = (n - (2 * i)) by A94, XREAL_1: 233;

            (n1 -' (2 * i)) = (1 + (n -' (2 * i))) by A96, A92;

            then

             A97: (a |^ (n1 -' (2 * i))) = (a * (a |^ (n -' (2 * i)))) by NEWTON: 6;

            

             A98: ((a * Fx) . i) = (a * (Fx . i)) by VALUED_1: 6

            .= (a * (((n choose (2 * i)) * (a |^ (n -' (2 * i)))) * (A |^ i))) by A95, A11, A88

            .= (((n choose (2 * i)) * (a |^ (n1 -' (2 * i)))) * (A |^ i)) by A97;

            

             A99: (((2 * i) -' 1) + 1) = (2 * i) by XREAL_1: 235, NAT_1: 14, A88;

            

            thus (FX . i) = ((AFx . i) + (AFy . i)) by RVSUM_1: 11

            .= ((((n choose ((2 * i) -' 1)) + (n choose (2 * i))) * (a |^ (n1 -' (2 * i)))) * (A |^ i)) by A90, A98

            .= (((n1 choose (2 * i)) * (a |^ (n1 -' (2 * i)))) * (A |^ i)) by A99, NEWTON: 22;

          end;

        end;

      end;

      for n holds P[n] from NAT_1:sch 2( A1, A7);

      hence thesis;

    end;

    begin

    theorem :: HILB10_1:10

    

     Th13: k <= n implies ( Px (a,k)) <= ( Px (a,n))

    proof

      assume k <= n;

      then

      reconsider nk = (n - k) as Nat by NAT_1: 21;

      defpred P[ Nat] means ( Px (a,k)) <= ( Px (a,(k + $1)));

      

       A1: P[ 0 ];

      

       A2: for i be Nat holds P[i] implies P[(i + 1)]

      proof

        let i be Nat;

        assume

         A3: P[i];

        

         A4: ( Px (a,((k + i) + 1))) = ((( Px (a,(k + i))) * a) + (( Py (a,(k + i))) * ((a ^2 ) -' 1))) by Th9;

        a >= 2 by NAT_2: 29;

        then a >= 1 by XXREAL_0: 2;

        then (( Px (a,(k + i))) * a) >= (( Px (a,(k + i))) * 1) by XREAL_1: 64;

        then ( Px (a,((k + i) + 1))) >= ((( Px (a,(k + i))) * 1) + 0 ) by A4, XREAL_1: 7;

        hence thesis by A3, XXREAL_0: 2;

      end;

       P[n1] from NAT_1:sch 2( A1, A2);

      then P[nk];

      hence thesis;

    end;

    registration

      let a, k;

      cluster ( Px (a,k)) -> positive;

      coherence

      proof

        ( Px (a, 0 )) = 1 & ( Px (a, 0 )) <= ( Px (a,k)) by Th6, Th13;

        hence thesis;

      end;

    end

    theorem :: HILB10_1:11

    

     Th14: k < n implies ( Py (a,k)) < ( Py (a,n))

    proof

      assume

       A1: k < n;

      then

      reconsider nk = (n - k) as Nat by NAT_1: 21;

      

       A2: nk <> 0 by A1;

      defpred P[ Nat] means $1 > 0 implies ( Py (a,k)) < ( Py (a,(k + $1)));

      

       A3: P[ 0 ];

      

       A4: for i be Nat holds P[i] implies P[(i + 1)]

      proof

        let i be Nat;

        assume

         A5: P[i];

        

         A6: ( Py (a,((k + i) + 1))) = ((( Py (a,(k + i))) * a) + ( Px (a,(k + i)))) by Th9;

        a >= 2 by NAT_2: 29;

        then a >= 1 by XXREAL_0: 2;

        then (( Py (a,(k + i))) * a) >= (( Py (a,(k + i))) * 1) by XREAL_1: 64;

        then

         A7: ( Py (a,((k + i) + 1))) > ((( Py (a,(k + i))) * 1) + 0 ) by A6, XREAL_1: 8;

        i = 0 or i > 0 ;

        hence thesis by A7, A5, XXREAL_0: 2;

      end;

       P[n1] from NAT_1:sch 2( A3, A4);

      then P[nk];

      hence thesis by A2;

    end;

    theorem :: HILB10_1:12

    

     Th15: ( Py (a,k)) = ( Py (a,n)) implies k = n

    proof

      assume ( Py (a,k)) = ( Py (a,n));

      then k >= n >= k by Th14;

      hence thesis by XXREAL_0: 1;

    end;

    theorem :: HILB10_1:13

    

     Th16: ( Py (a,n)) >= n

    proof

      defpred P[ Nat] means ( Py (a,$1)) >= $1;

      

       A1: P[ 0 ];

      

       A2: P[k] implies P[(k + 1)]

      proof

        (k + 1) > k by NAT_1: 13;

        then

         A3: (( Py (a,k)) + 1) <= ( Py (a,(k + 1))) by Th14, NAT_1: 13;

        assume P[k];

        then (k + 1) <= (( Py (a,k)) + 1) by XREAL_1: 6;

        hence thesis by A3, XXREAL_0: 2;

      end;

       P[k] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    

     Lm4: ( Py (a,k)) = 0 implies k = 0

    proof

      assume ( Py (a,k)) = 0 ;

      then ( Py (a,k)) = ( Py (a, 0 )) by Th6;

      hence thesis by Th15;

    end;

    registration

      let a;

      let k be non zero Nat;

      cluster ( Py (a,k)) -> non zero;

      coherence by Lm4;

    end

    registration

      let a be non trivial Nat;

      let x be positive Nat;

      cluster (a * x) -> non trivial;

      coherence

      proof

        a >= 2 & x >= 1 by NAT_1: 14, NAT_2: 29;

        then (a * x) >= (2 * 1) by XREAL_1: 66;

        then (a * x) <> 1;

        hence thesis by NAT_2: 28;

      end;

    end

    theorem :: HILB10_1:14

    

     Th17: a <> 2 & k <= n implies (2 * ( Py (a,k))) < ( Px (a,n))

    proof

      set A = ((a ^2 ) -' 1), S = ( sqrt A);

      

       A1: ((a ^2 ) -' 1) = ((a ^2 ) - 1) by NAT_1: 14, XREAL_1: 233;

      assume

       A2: a <> 2 & k <= n;

      ((( Px (a,k)) ^2 ) - (((a ^2 ) -' 1) * (( Py (a,k)) ^2 ))) = 1 by Th10;

      then

       A3: ((A * (( Py (a,k)) ^2 )) + 1) = (( Px (a,k)) ^2 );

      a >= (2 + 1) by A2, NAT_1: 22, NAT_2: 29;

      then (a ^2 ) >= (3 * 3) by XREAL_1: 66;

      then A >= (9 - 1) by A1, XREAL_1: 9;

      then A >= 4 by XXREAL_0: 2;

      then (4 * (( Py (a,k)) ^2 )) <= (A * (( Py (a,k)) ^2 )) by XREAL_1: 64;

      then ((2 * ( Py (a,k))) ^2 ) < (( Px (a,k)) ^2 ) by A3, NAT_1: 13;

      then

       A4: (2 * ( Py (a,k))) < ( Px (a,k)) by SQUARE_1: 15;

      ( Px (a,k)) <= ( Px (a,n)) by A2, Th13;

      hence thesis by A4, XXREAL_0: 2;

    end;

    theorem :: HILB10_1:15

    

     Th18: a = 2 & k <= n implies (( sqrt 3) * ( Py (a,k))) < ( Px (a,n))

    proof

      set A = ((a ^2 ) -' 1), S = ( sqrt A);

      

       A1: ((a ^2 ) -' 1) = ((a ^2 ) - 1) by NAT_1: 14, XREAL_1: 233;

      assume

       A2: a = 2 & k <= n;

      ((( Px (a,k)) ^2 ) - (((a ^2 ) -' 1) * (( Py (a,k)) ^2 ))) = 1 by Th10;

      then ((A * (( Py (a,k)) ^2 )) + 1) = (( Px (a,k)) ^2 );

      then

       A3: (3 * (( Py (a,k)) ^2 )) < (( Px (a,k)) ^2 ) by A1, A2, NAT_1: 13;

      (3 * (( Py (a,k)) ^2 )) = ((( sqrt 3) ^2 ) * (( Py (a,k)) ^2 )) by SQUARE_1:def 2

      .= ((( sqrt 3) * ( Py (a,k))) ^2 );

      then

       A4: (( sqrt 3) * ( Py (a,k))) < ( Px (a,k)) by A3, SQUARE_1: 15;

      ( Px (a,k)) <= ( Px (a,n)) by A2, Th13;

      hence thesis by A4, XXREAL_0: 2;

    end;

    theorem :: HILB10_1:16

    

     Th19: a = 2 & k < n implies ((3 + (2 * ( sqrt 3))) * ( Py (a,k))) < ( Px (a,n))

    proof

      

       A1: (( sqrt 3) ^2 ) = 3 & ( sqrt 3) >= 0 by SQUARE_1:def 2;

      set A = ((a ^2 ) -' 1), S = ( sqrt A);

      assume

       A2: a = 2 & k < n;

      then

       A3: (k + 1) <= n by NAT_1: 13;

      ( Py (a,(k + 1))) = (( Px (a,k)) + (( Py (a,k)) * a)) by Th9;

      then

       A4: (( sqrt 3) * (( Px (a,k)) + (( Py (a,k)) * 2))) < ( Px (a,n)) by A3, A2, Th18;

      (( sqrt 3) * ( Py (a,k))) <= ( Px (a,k)) by A2, Th18;

      then

       A5: ((( sqrt 3) * ( Py (a,k))) * ( sqrt 3)) <= (( Px (a,k)) * ( sqrt 3)) by A1, XREAL_1: 64;

      

       A6: ((( sqrt 3) * ( Py (a,k))) * ( sqrt 3)) = ((( sqrt 3) * ( sqrt 3)) * ( Py (a,k)))

      .= (3 * ( Py (a,k))) by A1;

      (( sqrt 3) * (( Px (a,k)) + (( Py (a,k)) * 2))) = ((( Py (a,k)) * (2 * ( sqrt 3))) + (( Px (a,k)) * ( sqrt 3)));

      then (( sqrt 3) * (( Px (a,k)) + (( Py (a,k)) * 2))) >= ((( Py (a,k)) * (2 * ( sqrt 3))) + (3 * ( Py (a,k)))) by A5, A6, XREAL_1: 7;

      hence thesis by A4, XXREAL_0: 2;

    end;

    theorem :: HILB10_1:17

    

     Th20: ((((2 * a) - 1) |^ n) * (a - 1)) <= ( Px (a,(n + 1))) <= (a * ((2 * a) |^ n)) & (((2 * a) - 1) |^ n) <= ( Py (a,(n + 1))) <= ((2 * a) |^ n)

    proof

      defpred P[ Nat] means (((2 * a) - 1) |^ $1) <= ( Py (a,($1 + 1))) <= ((2 * a) |^ $1) & ((((2 * a) - 1) |^ $1) * (a - 1)) <= ( Px (a,($1 + 1))) <= (a * ((2 * a) |^ $1));

      

       A1: ((a ^2 ) -' 1) = ((a ^2 ) - 1) by XREAL_1: 233, NAT_1: 14;

      

       A2: (((2 * a) - 1) |^ 0 ) = 1 & ((2 * a) |^ 0 ) = 1 by NEWTON: 4;

      

       A3: (a - 1) <= (a - 0 ) by XREAL_1: 10;

      ( Py (a, 0 )) = 0 & ( Px (a, 0 )) = 1 by Th6;

      then ( Py (a,(1 + 0 ))) = (1 + ( 0 * a)) & ( Px (a,(1 + 0 ))) = ((1 * a) + ( 0 * ((a ^2 ) -' 1))) by Th9;

      then

       A4: P[ 0 ] by A2, A3;

      

       A5: P[k] implies P[(k + 1)]

      proof

        set k1 = (k + 1);

        assume

         A6: P[k];

        

         A7: ( Py (a,(k1 + 1))) = (( Px (a,k1)) + (( Py (a,k1)) * a)) & ( Px (a,(k1 + 1))) = ((( Px (a,k1)) * a) + (( Py (a,k1)) * ((a ^2 ) -' 1))) by Th9;

        

         A8: (( Py (a,k1)) * a) <= (((2 * a) |^ k) * a) by A6, XREAL_1: 64;

        

         A9: ((((2 * a) |^ k) * a) + (((2 * a) |^ k) * a)) = (((2 * a) |^ k) * (2 * a))

        .= ((2 * a) |^ k1) by NEWTON: 6;

        

         A10: (( Py (a,k1)) * a) >= ((((2 * a) - 1) |^ k) * a) by A6, XREAL_1: 64;

        

         A11: (((((2 * a) - 1) |^ k) * (a - 1)) + ((((2 * a) - 1) |^ k) * a)) = ((((2 * a) - 1) |^ k) * ((2 * a) - 1))

        .= (((2 * a) - 1) |^ k1) by NEWTON: 6;

        (( Px (a,k1)) * a) <= ((a * ((2 * a) |^ k)) * a) & (( Py (a,k1)) * ((a ^2 ) -' 1)) <= (((2 * a) |^ k) * ((a ^2 ) -' 1)) by A6, XREAL_1: 64;

        then

         A12: ( Px (a,(k1 + 1))) <= (((a * ((2 * a) |^ k)) * a) + (((2 * a) |^ k) * ((a ^2 ) -' 1))) by A7, XREAL_1: 7;

        (((a ^2 ) + (a ^2 )) - 1) <= (((a ^2 ) + (a ^2 )) - 0 ) by XREAL_1: 10;

        then

         A13: (((2 * a) |^ k) * (((a ^2 ) + (a ^2 )) - 1)) <= (((2 * a) |^ k) * ((a ^2 ) + (a ^2 ))) by XREAL_1: 64;

        ((((2 * a) - 1) |^ k) * ((a ^2 ) -' 1)) <= (( Py (a,k1)) * ((a ^2 ) -' 1)) & (((((2 * a) - 1) |^ k) * (a - 1)) * a) <= (( Px (a,k1)) * a) by A6, XREAL_1: 64;

        then

         A14: (((((2 * a) - 1) |^ k) * ((a ^2 ) -' 1)) + (((((2 * a) - 1) |^ k) * (a - 1)) * a)) <= ( Px (a,(k1 + 1))) by A7, XREAL_1: 7;

        (2 * 1) <= (2 * a) by XREAL_1: 64, NAT_1: 14;

        then (1 - ( - 1)) <= (2 * a);

        then (((2 * (a ^2 )) - a) + (1 - (2 * a))) <= (((2 * (a ^2 )) - a) + ( - 1)) by XREAL_1: 6, XREAL_1: 12;

        then ((((2 * a) - 1) |^ k) * (((2 * a) - 1) * (a - 1))) <= ((((2 * a) - 1) |^ k) * (((a ^2 ) - 1) + ((a - 1) * a))) by XREAL_1: 64;

        hence thesis by A8, A7, A6, XREAL_1: 7, A9, A10, A11, A1, A13, A12, XXREAL_0: 2, A14;

      end;

       P[k] from NAT_1:sch 2( A4, A5);

      hence thesis;

    end;

    theorem :: HILB10_1:18

    

     Th21: for x be positive Nat holds ((x |^ n) * ((1 - (1 / ((2 * a) * x))) |^ n)) <= (( Py ((a * x),(n + 1))) / ( Py (a,(n + 1)))) <= ((x |^ n) * (1 / ((1 - (1 / (2 * a))) |^ n)))

    proof

      let x be positive Nat;

      set z = n;

      (1 - (1 / ((2 * a) * x))) = ((((2 * a) * x) / ((2 * a) * x)) - (1 / ((2 * a) * x))) by XCMPLX_1: 60

      .= ((((2 * a) * x) - 1) / ((2 * a) * x)) by XCMPLX_1: 120;

      then (x * (1 - (1 / ((2 * a) * x)))) = ((((2 * a) * x) - 1) / (2 * a)) by XCMPLX_1: 92;

      

      then

       A1: ((x |^ z) * ((1 - (1 / ((2 * a) * x))) |^ z)) = (((((2 * a) * x) - 1) / (2 * a)) to_power z) by NEWTON: 7

      .= (((((2 * a) * x) - 1) to_power z) / ((2 * a) to_power z)) by POWER: 31;

      

       A2: (((2 * a) - 1) |^ z) <= ( Py (a,(z + 1))) <= ((2 * a) |^ z) by Th20;

      

       A3: (((2 * (a * x)) - 1) |^ z) <= ( Py ((a * x),(z + 1))) <= ((2 * (a * x)) |^ z) by Th20;

      (((((2 * a) * x) - 1) |^ z) * ( Py (a,(z + 1)))) <= (( Py ((a * x),(z + 1))) * ((2 * a) |^ z)) by A2, A3, XREAL_1: 66;

      hence ((x |^ z) * ((1 - (1 / ((2 * a) * x))) |^ z)) <= (( Py ((a * x),(z + 1))) / ( Py (a,(z + 1)))) by A1, XREAL_1: 102;

      a >= 1 by NAT_1: 14;

      then (a + a) >= (1 + 1) by XREAL_1: 7;

      then (1 * (2 * a)) > 1 by NAT_1: 13;

      then 1 > (1 / (2 * a)) by XREAL_1: 83;

      then

       A4: (1 - (1 / (2 * a))) > ((1 / (2 * a)) - (1 / (2 * a))) by XREAL_1: 14;

      

       A5: (( Py ((a * x),(z + 1))) * (((2 * a) - 1) |^ z)) <= ((((2 * a) * x) |^ z) * ( Py (a,(z + 1)))) by A2, A3, XREAL_1: 66;

      ((2 * a) / (2 * a)) = 1 by XCMPLX_1: 60;

      then (((2 * a) - 1) / (2 * a)) = (1 - (1 / (2 * a))) by XCMPLX_1: 120;

      then ((2 * a) / ((2 * a) - 1)) = (1 / (1 - (1 / (2 * a)))) by XCMPLX_1: 57;

      then (((2 * a) * x) / ((2 * a) - 1)) = (x * (1 / (1 - (1 / (2 * a))))) by XCMPLX_1: 74;

      then (((2 * a) * x) / ((2 * a) - 1)) = ((x * 1) / (1 - (1 / (2 * a)))) by XCMPLX_1: 74;

      

      then ((((2 * a) * x) to_power z) / (((2 * a) - 1) to_power z)) = ((x / (1 - (1 / (2 * a)))) to_power z) by POWER: 31

      .= ((1 * (x to_power z)) / ((1 - (1 / (2 * a))) to_power z)) by A4, POWER: 31

      .= ((x |^ z) * (1 / ((1 - (1 / (2 * a))) |^ z))) by XCMPLX_1: 74;

      hence thesis by A5, XREAL_1: 102;

    end;

    

     Lm5: 0 <= (1 - r) <= 1 implies ((1 - r) |^ n) >= (1 - (n * r))

    proof

      defpred P[ Nat] means (1 - ($1 * r)) >= 0 implies ((1 - r) |^ $1) >= (1 - ($1 * r));

      assume

       A1: 0 <= (1 - r) <= 1;

      (1 - 0 ) = 1;

      then

       A2: r >= 0 by A1, XREAL_1: 10;

      

       A3: P[ 0 ] by NEWTON: 4;

      

       A4: P[k] implies P[(k + 1)]

      proof

        assume

         A5: P[k];

        

         A6: ((1 - r) |^ (k + 1)) = ((1 - r) * ((1 - r) |^ k)) by NEWTON: 6;

        assume (1 - ((k + 1) * r)) >= 0 ;

        then (((1 - (k * r)) - r) + r) >= ( 0 + r) by XREAL_1: 6;

        then (1 - (k * r)) >= 0 ;

        then

         A7: ((1 - r) |^ (k + 1)) >= ((1 - r) * (1 - (k * r))) by A5, A6, A1, XREAL_1: 66;

        (((1 - (k * r)) - r) + ((r * r) * k)) >= (((1 - (k * r)) - r) + 0 ) by A2, XREAL_1: 7;

        hence thesis by A7, XXREAL_0: 2;

      end;

      

       A8: P[k] from NAT_1:sch 2( A3, A4);

      (1 - (n * r)) >= 0 or (1 - (n * r)) < 0 ;

      hence thesis by A8, A1;

    end;

    theorem :: HILB10_1:19

    

     Th22: for x be positive Nat st a > ((2 * n) * (x |^ n)) holds ((x |^ n) - (1 / 2)) < (( Py ((a * x),(n + 1))) / ( Py (a,(n + 1)))) < ((x |^ n) + (1 / 2))

    proof

      let x be positive Nat;

      

       A1: ((x |^ n) * ((1 - (1 / ((2 * a) * x))) |^ n)) <= (( Py ((a * x),(n + 1))) / ( Py (a,(n + 1)))) <= ((x |^ n) * (1 / ((1 - (1 / (2 * a))) |^ n))) by Th21;

      assume

       A2: a > ((2 * n) * (x |^ n));

      

       A3: (1 - (n * (1 / (2 * a)))) = (1 - ((n * 1) / (2 * a))) by XCMPLX_1: 74;

      ((2 * (x |^ n)) * n) >= (1 * n) by XREAL_1: 64, NAT_1: 14;

      then a >= n by A2, XXREAL_0: 2;

      then (a - n) >= (n - n) by XREAL_1: 9;

      then

       A4: ((a - n) + a) >= (a + 0 ) by XREAL_1: 6;

      then (n / ((2 * a) - n)) <= (n / a) by XREAL_1: 118;

      then (1 + (n / ((2 * a) - n))) <= (1 + (n / a)) by XREAL_1: 6;

      then

       A5: ((x |^ n) * (1 + (n / ((2 * a) - n)))) <= ((x |^ n) * (1 + (n / a))) by XREAL_1: 64;

      

       A6: ((2 * a) - n) > 0 by A4;

      

       A7: (1 / 1) >= (1 / (2 * a)) by XREAL_1: 118, NAT_1: 14;

      (2 * a) > n by A6, XREAL_1: 47;

      then (n / (2 * a)) < 1 by XREAL_1: 191;

      then

       A8: (1 - (n / (2 * a))) > (1 - 1) by XREAL_1: 10;

      (1 - 1) <= (1 - (1 / (2 * a))) <= (1 - 0 ) by A7, XREAL_1: 10;

      then ((1 - (1 / (2 * a))) |^ n) >= (1 - (n / (2 * a))) by Lm5, A3;

      then (1 / ((1 - (1 / (2 * a))) |^ n)) <= (1 / (1 - (n / (2 * a)))) by A8, XREAL_1: 118;

      then

       A9: ((x |^ n) * (1 / ((1 - (1 / (2 * a))) |^ n))) <= ((x |^ n) * (1 / (1 - (n / (2 * a))))) by XREAL_1: 64;

      (1 - (n / (2 * a))) = (((2 * a) / (2 * a)) - (n / (2 * a))) by XCMPLX_1: 60

      .= (((2 * a) - n) / (2 * a)) by XCMPLX_1: 120;

      

      then

       A10: (1 / (1 - (n / (2 * a)))) = ((((2 * a) - n) + n) / ((2 * a) - n)) by XCMPLX_1: 57

      .= ((((2 * a) - n) / ((2 * a) - n)) + (n / ((2 * a) - n))) by XCMPLX_1: 62

      .= (1 + (n / ((2 * a) - n))) by XCMPLX_1: 60, A4;

      

       A11: ((x |^ n) * (1 / ((1 - (1 / (2 * a))) |^ n))) <= ((x |^ n) * (1 + (n / a))) by A5, A9, A10, XXREAL_0: 2;

      ((2 * n) * (x |^ n)) = (2 * (n * (x |^ n)));

      then (n * (x |^ n)) < (a / 2) by A2, XREAL_1: 81;

      then (n * (x |^ n)) < ((1 / 2) * a);

      then ((n * (x |^ n)) / a) < (1 / 2) by XREAL_1: 83;

      then ((n / a) * (x |^ n)) < (1 / 2) by XCMPLX_1: 74;

      then ((x |^ n) + ((x |^ n) * (n / a))) < ((x |^ n) + (1 / 2)) by XREAL_1: 6;

      then

       A12: ((x |^ n) * (1 / ((1 - (1 / (2 * a))) |^ n))) < ((x |^ n) + (1 / 2)) by A11, XXREAL_0: 2;

      1 >= (1 / ((2 * a) * x)) by XREAL_1: 185, NAT_1: 14;

      then (1 - 1) <= (1 - (1 / ((2 * a) * x))) <= (1 - 0 ) by XREAL_1: 10;

      then

       A13: ((x |^ n) * ((1 - (1 / ((2 * a) * x))) |^ n)) >= ((x |^ n) * (1 - (n * (1 / ((2 * a) * x))))) by Lm5, XREAL_1: 64;

      (((x |^ n) * (n * (1 / ((2 * a) * x)))) * 2) = (((x |^ n) * ((n * 1) / ((2 * a) * x))) * 2) by XCMPLX_1: 74

      .= (((x |^ n) * 2) * (n / ((2 * a) * x)))

      .= ((((x |^ n) * 2) * n) / ((2 * a) * x)) by XCMPLX_1: 74;

      then

       A14: (((x |^ n) * (n * (1 / ((2 * a) * x)))) * 2) < (a / ((2 * a) * x)) by A2, XREAL_1: 74;

      ((2 * x) * a) >= (1 * a) by XREAL_1: 64, NAT_1: 14;

      then (a / ((2 * a) * x)) <= 1 by XREAL_1: 183;

      then (((x |^ n) * (n * (1 / ((2 * a) * x)))) * 2) < 1 by A14, XXREAL_0: 2;

      then ((x |^ n) * (n * (1 / ((2 * a) * x)))) < (1 / 2) by XREAL_1: 81;

      then ((x |^ n) - ((x |^ n) * (n * (1 / ((2 * a) * x))))) > ((x |^ n) - (1 / 2)) by XREAL_1: 15;

      then ((x |^ n) * ((1 - (1 / ((2 * a) * x))) |^ n)) > ((x |^ n) - (1 / 2)) by A13, XXREAL_0: 2;

      hence thesis by A12, A1, XXREAL_0: 2;

    end;

    begin

    theorem :: HILB10_1:20

    

     Th23: x >= 0 implies (( sgn x) * ( Py (a, |.x.|))) = ( Py (a, |.x.|))

    proof

      assume x >= 0 ;

      then x = 0 or x > 0 ;

      then ( sgn x) = 1 or (( sgn x) = 0 & x = 0 ) by ABSVALUE:def 2;

      hence thesis by Th6;

    end;

    theorem :: HILB10_1:21

    

     Th24: x <= 0 implies (( sgn x) * ( Py (a, |.x.|))) = ( - ( Py (a, |.x.|)))

    proof

      

       A1: ( Py (a, |. 0 .|)) = 0 by Th6;

      assume x <= 0 ;

      then x = 0 or x < 0 ;

      then ( sgn x) = ( - 1) or (( sgn x) = 0 & x = 0 ) by ABSVALUE:def 2;

      hence thesis by A1;

    end;

    theorem :: HILB10_1:22

    

     Th25: ( Px (a, |.(x + y).|)) = ((( Px (a, |.x.|)) * ( Px (a, |.y.|))) + ((((((a ^2 ) -' 1) * ( sgn x)) * ( Py (a, |.x.|))) * ( sgn y)) * ( Py (a, |.y.|)))) & (( sgn (x + y)) * ( Py (a, |.(x + y).|))) = (((( Px (a, |.x.|)) * ( sgn y)) * ( Py (a, |.y.|))) + ((( sgn x) * ( Py (a, |.x.|))) * ( Px (a, |.y.|))))

    proof

      set i = x, j = y, I = |.x.|, J = |.y.|, IJ = |.(x + y).|;

      set A = ((a ^2 ) -' 1), S = ( sqrt A);

      

       A1: ((a ^2 ) -' 1) = ((a ^2 ) - 1) by NAT_1: 14, XREAL_1: 233;

      

       A2: (S ^2 ) = A by SQUARE_1:def 2;

      

       A3: 1 = (((a + S) * (a - S)) |^ I) by A2, A1

      .= (((a + S) |^ I) * ((a - S) |^ I)) by NEWTON: 7;

      

       A4: 1 = (((a + S) * (a - S)) |^ J) by A2, A1

      .= (((a + S) |^ J) * ((a - S) |^ J)) by NEWTON: 7;

      deffunc PX( Integer) = ( Px (a, |.$1.|));

      deffunc PY( Integer) = (( sgn $1) * ( Py (a, |.$1.|)));

      per cases ;

        suppose

         A5: i >= 0 & j >= 0 ;

        then

         A6: i = I & j = J by ABSVALUE:def 1;

        

         A7: PY(i) = ( Py (a,I)) by Th23, A5;

        

         A8: PY(j) = ( Py (a,J)) by A5, Th23;

        

         A9: IJ = (i + j) by A5, ABSVALUE:def 1;

         PY(+) = ( Py (a,IJ)) by Th23, A5;

        

        then ( PX(+) + ( PY(+) * S)) = ((a + S) |^ IJ) by Th11

        .= (((a + S) |^ I) * ((a + S) |^ J)) by A6, A9, NEWTON: 8

        .= (( PX(i) + ( PY(i) * S)) * ((a + S) |^ J)) by A7, Th11

        .= (( PX(i) + ( PY(i) * S)) * ( PX(j) + ( PY(j) * S))) by A8, Th11

        .= ((( PX(i) * PX(j)) + ((A * PY(i)) * PY(j))) + (S * (( PX(i) * PY(j)) + ( PY(i) * PX(j))))) by A2;

        hence thesis by PELLS_EQ: 3;

      end;

        suppose

         A10: i < 0 & j >= 0 ;

        then

         A11: ( - i) = I & j = J by ABSVALUE:def 1;

        

         A12: PY(i) = ( - ( Py (a,I))) by A10, Th24;

        

         A13: PY(j) = ( Py (a,J)) by A10, Th23;

        per cases ;

          suppose

           A14: (i + j) >= 0 ;

          then IJ = (i + j) by ABSVALUE:def 1;

          then

           A15: (IJ + I) = J by A11;

           PY(+) = ( Py (a,IJ)) by A14, Th23;

          

          then ( PX(+) + ( PY(+) * S)) = (((a + S) |^ IJ) * (((a + S) |^ I) * ((a - S) |^ I))) by Th11, A3

          .= ((((a + S) |^ IJ) * ((a + S) |^ I)) * ((a - S) |^ I))

          .= (((a + S) |^ J) * ((a - S) |^ I)) by A15, NEWTON: 8

          .= (( PX(j) + ( PY(j) * S)) * ((a - S) |^ I)) by A13, Th11

          .= (( PX(j) + ( PY(j) * S)) * ( PX(i) + ( PY(i) * S))) by A12, Th11

          .= ((( PX(i) * PX(j)) + ((A * PY(i)) * PY(j))) + (S * (( PX(i) * PY(j)) + ( PY(i) * PX(j))))) by A2;

          hence thesis by PELLS_EQ: 3;

        end;

          suppose

           A16: (i + j) < 0 ;

          then IJ = ( - (i + j)) by ABSVALUE:def 1;

          then

           A17: (IJ + J) = I by A11;

           PY(+) = ( - ( Py (a,IJ))) by A16, Th24;

          

          then ( PX(+) + ( PY(+) * S)) = (((a - S) |^ IJ) * (((a + S) |^ J) * ((a - S) |^ J))) by Th11, A4

          .= ((((a - S) |^ IJ) * ((a - S) |^ J)) * ((a + S) |^ J))

          .= (((a - S) |^ I) * ((a + S) |^ J)) by A17, NEWTON: 8

          .= (( PX(i) + ( PY(i) * S)) * ((a + S) |^ J)) by A12, Th11

          .= (( PX(i) + ( PY(i) * S)) * ( PX(j) + ( PY(j) * S))) by A13, Th11

          .= ((( PX(i) * PX(j)) + ((A * PY(i)) * PY(j))) + (S * (( PX(i) * PY(j)) + ( PY(i) * PX(j))))) by A2;

          hence thesis by PELLS_EQ: 3;

        end;

      end;

        suppose

         A18: i >= 0 & j < 0 ;

        then

         A19: i = I & ( - j) = J by ABSVALUE:def 1;

        

         A20: PY(i) = ( Py (a,I)) by Th23, A18;

        

         A21: PY(j) = ( - ( Py (a,J))) by A18, Th24;

        per cases ;

          suppose

           A22: (i + j) >= 0 ;

          then IJ = (i + j) by ABSVALUE:def 1;

          then

           A23: (IJ + J) = I by A19;

           PY(+) = ( Py (a,IJ)) by A22, Th23;

          

          then ( PX(+) + ( PY(+) * S)) = (((a + S) |^ IJ) * (((a + S) |^ J) * ((a - S) |^ J))) by A4, Th11

          .= ((((a + S) |^ IJ) * ((a + S) |^ J)) * ((a - S) |^ J))

          .= (((a + S) |^ I) * ((a - S) |^ J)) by A23, NEWTON: 8

          .= (( PX(i) + ( PY(i) * S)) * ((a - S) |^ J)) by A20, Th11

          .= (( PX(i) + ( PY(i) * S)) * ( PX(j) + ( PY(j) * S))) by A21, Th11

          .= ((( PX(i) * PX(j)) + ((A * PY(i)) * PY(j))) + (S * (( PX(i) * PY(j)) + ( PY(i) * PX(j))))) by A2;

          hence thesis by PELLS_EQ: 3;

        end;

          suppose

           A24: (i + j) < 0 ;

          then IJ = ( - (i + j)) by ABSVALUE:def 1;

          then

           A25: (IJ + I) = J by A19;

           PY(+) = ( - ( Py (a,IJ))) by A24, Th24;

          

          then ( PX(+) + ( PY(+) * S)) = (((a - S) |^ IJ) * (((a - S) |^ I) * ((a + S) |^ I))) by Th11, A3

          .= ((((a - S) |^ IJ) * ((a - S) |^ I)) * ((a + S) |^ I))

          .= (((a - S) |^ J) * ((a + S) |^ I)) by A25, NEWTON: 8

          .= (( PX(j) + ( PY(j) * S)) * ((a + S) |^ I)) by A21, Th11

          .= (( PX(j) + ( PY(j) * S)) * ( PX(i) + ( PY(i) * S))) by A20, Th11

          .= ((( PX(i) * PX(j)) + ((A * PY(i)) * PY(j))) + (S * (( PX(i) * PY(j)) + ( PY(i) * PX(j))))) by A2;

          hence thesis by PELLS_EQ: 3;

        end;

      end;

        suppose

         A26: i < 0 & j < 0 ;

        then

         A27: ( - i) = I & ( - j) = J by ABSVALUE:def 1;

        

         A28: PY(i) = ( - ( Py (a,I))) by A26, Th24;

        

         A29: PY(j) = ( - ( Py (a,J))) by A26, Th24;

        

         A30: IJ = ( - (i + j)) by A26, ABSVALUE:def 1;

        

         A31: IJ = (I + J) by A27, A30;

        ( PX(+) + ( PY(+) * S)) = ( PX(+) + (( - ( Py (a,IJ))) * S)) by A26, Th24

        .= ((a - S) |^ IJ) by Th11

        .= (((a - S) |^ I) * ((a - S) |^ J)) by A31, NEWTON: 8

        .= (( PX(i) + ( PY(i) * S)) * ((a - S) |^ J)) by A28, Th11

        .= (( PX(i) + ( PY(i) * S)) * ( PX(j) + ( PY(j) * S))) by A29, Th11

        .= ((( PX(i) * PX(j)) + ((A * PY(i)) * PY(j))) + (S * (( PX(i) * PY(j)) + ( PY(i) * PX(j))))) by A2;

        hence thesis by PELLS_EQ: 3;

      end;

    end;

    begin

    theorem :: HILB10_1:23

    

     Th26: (( Px (a,n)),( Py (a,n))) are_coprime

    proof

      defpred P[ Nat] means (( Px (a,$1)) gcd ( Py (a,$1))) = 1;

      ( Px (a, 0 )) = 1 & ( Py (a, 0 )) = 0 by Th6;

      then

       A1: P[ 0 ];

      

       A2: for n st P[n] holds P[(n + 1)]

      proof

        set A = ((a ^2 ) -' 1);

        

         A3: A = ((a ^2 ) - 1) by NAT_1: 14, XREAL_1: 233;

        let n such that

         A4: P[n];

        

         A5: ( Px (a,(n + 1))) = ((( Px (a,n)) * a) + (( Py (a,n)) * A)) & ( Py (a,(n + 1))) = (( Px (a,n)) + (( Py (a,n)) * a)) by Th9;

        

        thus 1 = ((( Px (a,n)) + (( Py (a,n)) * a)) gcd ( Py (a,n))) by A4, EULER_1: 8

        .= (( Py (a,(n + 1))) gcd ( - ( Py (a,n)))) by A5, NEWTON02: 1

        .= ((( - ( Py (a,n))) + (a * ( Py (a,(n + 1))))) gcd ( Py (a,(n + 1)))) by NEWTON02: 5

        .= (( Px (a,(n + 1))) gcd ( Py (a,(n + 1)))) by A3, A5;

      end;

      for n holds P[n] from NAT_1:sch 2( A1, A2);

      then (( Px (a,n)) gcd ( Py (a,n))) = 1;

      hence thesis by INT_2:def 3;

    end;

    theorem :: HILB10_1:24

    

     Th27: (( Py (a,n)),n) are_congruent_mod (a - 1)

    proof

      set A = (a - 1);

      

       A1: ((a ^2 ) -' 1) = ((a ^2 ) - 1) by NAT_1: 14, XREAL_1: 233;

      consider Fy,Fx be FinSequence of NAT such that

       A2: ( Sum Fy) = ( Py (a,n)) & ( len Fy) = [\((n + 1) / 2)/] and

       A3: for i be Nat st 1 <= i <= ((n + 1) / 2) holds (Fy . i) = (((n choose ((2 * i) -' 1)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2 ) -' 1) |^ (i -' 1))) and ((a |^ n) + ( Sum Fx)) = ( Px (a,n)) & ( len Fx) = [\(n / 2)/] & for i be Nat st 1 <= i <= (n / 2) holds (Fx . i) = (((n choose (2 * i)) * (a |^ (n -' (2 * i)))) * (((a ^2 ) -' 1) |^ i)) by Th12;

      per cases ;

        suppose

         A4: n = 0 ;

        then ( Py (a,n)) = 0 by Th6;

        hence thesis by A4, INT_1: 11;

      end;

        suppose

         A5: n <> 0 ;

        for i be Nat st 1 < i <= ( len Fy) holds ((Fy . i) mod A) = 0

        proof

          let i be Nat such that

           A6: 1 < i <= ( len Fy);

          (i -' 1) = (i - 1) by A6, XREAL_1: 233;

          then (i -' 1) <> 0 by A6;

          then

          reconsider ii = ((i -' 1) - 1) as Element of NAT by NAT_1: 20;

          (i -' 1) = (ii + 1);

          then

           A7: (((a ^2 ) -' 1) |^ (i -' 1)) = ((A * (a + 1)) * (((a ^2 ) -' 1) |^ ii)) by A1, NEWTON: 6;

           [\((n + 1) / 2)/] <= ((n + 1) / 2) by INT_1:def 6;

          then i <= ((n + 1) / 2) by A2, A6, XXREAL_0: 2;

          

          then (Fy . i) = (((n choose ((2 * i) -' 1)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2 ) -' 1) |^ (i -' 1))) by A6, A3

          .= (((((n choose ((2 * i) -' 1)) * (a |^ ((n + 1) -' (2 * i)))) * (a + 1)) * (((a ^2 ) -' 1) |^ ii)) * A) by A7;

          then A divides (Fy . i) by INT_1:def 3;

          hence thesis by INT_1: 62;

        end;

        then (( Py (a,n)) mod A) = ((Fy . 1) mod A) by Th1, A2;

        then ((( Py (a,n)) - (Fy . 1)) mod A) = 0 by INT_4: 22;

        then A divides (( Py (a,n)) - (Fy . 1)) by INT_1: 62;

        then

         A8: (( Py (a,n)),(Fy . 1)) are_congruent_mod A by INT_1:def 4;

        n >= 1 by A5, NAT_1: 14;

        then (n + 1) >= (1 + 1) & (1 + 1) = (2 * 1) by XREAL_1: 7;

        then

         A9: ((n + 1) / 2) >= 1 by XREAL_1: 77;

        (1 -' 1) = (1 - 1) by XREAL_1: 233;

        then

         A10: (((a ^2 ) -' 1) |^ (1 -' 1)) = 1 by NEWTON: 4;

        ((2 * 1) -' 1) = (2 - 1) by XREAL_1: 233;

        then

         A11: (n choose ((2 * 1) -' 1)) = n by A5, NAT_1: 14, NEWTON: 23;

        

         A12: (Fy . 1) = ((n * (a |^ ((n + 1) -' (2 * 1)))) * 1) by A9, A10, A11, A3;

        

         A13: A >= (2 - 1) by NAT_2: 29, XREAL_1: 9;

        per cases by A13, XXREAL_0: 1;

          suppose A = 1;

          then (A * (( Py (a,n)) - n)) = (( Py (a,n)) - n);

          hence thesis by INT_1:def 5;

        end;

          suppose

           A14: A > 1;

          a = ((A * 1) + 1);

          

          then (a mod A) = (1 mod A) by PEPIN: 10

          .= 1 by A14, PEPIN: 5;

          then ((a |^ ((n + 1) -' (2 * 1))) mod A) = 1 by A14, PEPIN: 35;

          then ((a |^ ((n + 1) -' (2 * 1))),1) are_congruent_mod A by A14, PEPIN: 39;

          then ((Fy . 1),(1 * n)) are_congruent_mod A by A12, INT_4: 11;

          hence thesis by A8, INT_1: 15;

        end;

      end;

    end;

    theorem :: HILB10_1:25

    

     Th28: (( Px (a,n)),( Px (b,n))) are_congruent_mod (a - b) & (( Py (a,n)),( Py (b,n))) are_congruent_mod (a - b)

    proof

      defpred P[ Nat] means (( Px (a,$1)),( Px (b,$1))) are_congruent_mod (a - b) & (( Py (a,$1)),( Py (b,$1))) are_congruent_mod (a - b);

      ( Px (a, 0 )) = 1 = ( Px (b, 0 )) & ( Py (a, 0 )) = 0 = ( Py (b, 0 )) by Th6;

      then

       A1: P[ 0 ] by INT_1: 11;

      

       A2: for n st P[n] holds P[(n + 1)]

      proof

        set A = ((a ^2 ) -' 1), B = ((b ^2 ) -' 1);

        A = ((a ^2 ) - 1) & B = ((b ^2 ) - 1) by NAT_1: 14, XREAL_1: 233;

        then (A - B) = ((a - b) * (a + b));

        then

         A3: (A,B) are_congruent_mod (a - b) by INT_1:def 5;

        (a - b) = (1 * (a - b));

        then

         A4: (a,b) are_congruent_mod (a - b) by INT_1:def 5;

        let n such that

         A5: P[n];

        

         A6: ( Px (a,(n + 1))) = ((( Px (a,n)) * a) + (( Py (a,n)) * A)) & ( Px (b,(n + 1))) = ((( Px (b,n)) * b) + (( Py (b,n)) * B)) by Th9;

        

         A7: ((( Py (a,n)) * A),(( Py (b,n)) * B)) are_congruent_mod (a - b) by A5, A3, INT_1: 18;

        ((( Px (a,n)) * a),(( Px (b,n)) * b)) are_congruent_mod (a - b) by A5, A4, INT_1: 18;

        hence (( Px (a,(n + 1))),( Px (b,(n + 1)))) are_congruent_mod (a - b) by A6, A7, INT_1: 16;

        

         A8: ( Py (a,(n + 1))) = (( Px (a,n)) + (( Py (a,n)) * a)) & ( Py (b,(n + 1))) = (( Px (b,n)) + (( Py (b,n)) * b)) by Th9;

        ((( Py (a,n)) * a),(( Py (b,n)) * b)) are_congruent_mod (a - b) by A4, A5, INT_1: 18;

        hence (( Py (a,(n + 1))),( Py (b,(n + 1)))) are_congruent_mod (a - b) by A8, A5, INT_1: 16;

      end;

      for n holds P[n] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    theorem :: HILB10_1:26

    

     Th29: (a,b) are_congruent_mod k implies (( Py (a,n)),( Py (b,n))) are_congruent_mod k

    proof

      assume (a,b) are_congruent_mod k;

      then

      consider x be Integer such that

       A1: (k * x) = (a - b) by INT_1:def 5;

      consider p be Integer such that

       A2: ((a - b) * p) = (( Py (a,n)) - ( Py (b,n))) by Th28, INT_1:def 5;

      (p * (a - b)) = (p * (x * k)) by A1

      .= ((p * x) * k);

      hence thesis by A2, INT_1:def 5;

    end;

    

     Lm6: ((( sgn x) * ( sgn x)) * ( Py (a, |.x.|))) = ( Py (a, |.x.|))

    proof

      per cases ;

        suppose

         A1: x >= 0 ;

        

        thus ((( sgn x) * ( sgn x)) * ( Py (a, |.x.|))) = (( sgn x) * (( sgn x) * ( Py (a, |.x.|))))

        .= (( sgn x) * ( Py (a, |.x.|))) by A1, Th23

        .= ( Py (a, |.x.|)) by A1, Th23;

      end;

        suppose

         A2: x <= 0 ;

        

        thus ((( sgn x) * ( sgn x)) * ( Py (a, |.x.|))) = (( sgn x) * (( sgn x) * ( Py (a, |.x.|))))

        .= (( sgn x) * ( - ( Py (a, |.x.|)))) by A2, Th24

        .= ( - (( sgn x) * ( Py (a, |.x.|))))

        .= ( - ( - ( Py (a, |.x.|)))) by A2, Th24

        .= ( Py (a, |.x.|));

      end;

    end;

    theorem :: HILB10_1:27

    

     Th30: ((( sgn ((2 * x) + y)) * ( Py (a, |.((2 * x) + y).|))),( - (( sgn y) * ( Py (a, |.y.|))))) are_congruent_mod ( Px (a, |.x.|))

    proof

      set i = x, j = y, A = ((a ^2 ) -' 1);

      ((2 * i) + j) = (i + (i + j));

      then (( sgn ((2 * i) + j)) * ( Py (a, |.((2 * i) + j).|))) = (((( Px (a, |.i.|)) * ( sgn (i + j))) * ( Py (a, |.(i + j).|))) + ((( sgn i) * ( Py (a, |.i.|))) * ( Px (a, |.(i + j).|)))) by Th25;

      then ((( sgn ((2 * i) + j)) * ( Py (a, |.((2 * i) + j).|))) - ((( sgn i) * ( Py (a, |.i.|))) * ( Px (a, |.(i + j).|)))) = (( Px (a, |.i.|)) * (( sgn (i + j)) * ( Py (a, |.(i + j).|))));

      then

       A1: ((( sgn ((2 * i) + j)) * ( Py (a, |.((2 * i) + j).|))),((( sgn i) * ( Py (a, |.i.|))) * ( Px (a, |.(i + j).|)))) are_congruent_mod ( Px (a, |.i.|)) by INT_1:def 5;

      

       A2: ((( sgn i) * ( Py (a, |.i.|))) * ((((A * ( sgn i)) * ( Py (a, |.i.|))) * ( sgn j)) * ( Py (a, |.j.|)))) = ((((((( sgn i) * ( sgn i)) * ( Py (a, |.i.|))) * ((a ^2 ) -' 1)) * ( Py (a, |.i.|))) * ( sgn j)) * ( Py (a, |.j.|)))

      .= ((((( Py (a, |.i.|)) * A) * ( Py (a, |.i.|))) * ( sgn j)) * ( Py (a, |.j.|))) by Lm6;

      

       A3: ((( Px (a, |.i.|)) ^2 ) - (((a ^2 ) -' 1) * (( Py (a, |.i.|)) ^2 ))) = 1 by Th10;

      ( Px (a, |.(i + j).|)) = ((( Px (a, |.i.|)) * ( Px (a, |.j.|))) + ((((((a ^2 ) -' 1) * ( sgn i)) * ( Py (a, |.i.|))) * ( sgn j)) * ( Py (a, |.j.|)))) by Th25;

      then (( Px (a, |.(i + j).|)) - ((((((a ^2 ) -' 1) * ( sgn i)) * ( Py (a, |.i.|))) * ( sgn j)) * ( Py (a, |.j.|)))) = (( Px (a, |.i.|)) * ( Px (a, |.j.|)));

      then (( Px (a, |.(i + j).|)),((((((a ^2 ) -' 1) * ( sgn i)) * ( Py (a, |.i.|))) * ( sgn j)) * ( Py (a, |.j.|)))) are_congruent_mod ( Px (a, |.i.|)) by INT_1:def 5;

      then (((( sgn i) * ( Py (a, |.i.|))) * ( Px (a, |.(i + j).|))),((((( Py (a, |.i.|)) * A) * ( Py (a, |.i.|))) * ( sgn j)) * ( Py (a, |.j.|)))) are_congruent_mod ( Px (a, |.i.|)) by A2, INT_4: 11;

      then

       A4: ((( sgn ((2 * i) + j)) * ( Py (a, |.((2 * i) + j).|))),((((( Px (a, |.i.|)) ^2 ) - 1) * ( sgn j)) * ( Py (a, |.j.|)))) are_congruent_mod ( Px (a, |.i.|)) by A3, A1, INT_1: 15;

      (((((( Px (a, |.i.|)) ^2 ) - 1) * ( sgn j)) * ( Py (a, |.j.|))) - ( - (( sgn j) * ( Py (a, |.j.|))))) = (( Px (a, |.i.|)) * ((( Px (a, |.i.|)) * ( sgn j)) * ( Py (a, |.j.|))));

      then (((((( Px (a, |.i.|)) ^2 ) - 1) * ( sgn j)) * ( Py (a, |.j.|))),( - (( sgn j) * ( Py (a, |.j.|))))) are_congruent_mod ( Px (a, |.i.|)) by INT_1:def 5;

      hence thesis by A4, INT_1: 15;

    end;

    

     Lm7: for i,j be Integer holds ((( sgn ((4 * i) + j)) * ( Py (a, |.((4 * i) + j).|))),(( sgn j) * ( Py (a, |.j.|)))) are_congruent_mod ( Px (a, |.i.|))

    proof

      let i,j be Integer;

      ((4 * i) + j) = ((2 * i) + ((2 * i) + j));

      then

       A1: ((( sgn ((4 * i) + j)) * ( Py (a, |.((4 * i) + j).|))),( - (( sgn ((2 * i) + j)) * ( Py (a, |.((2 * i) + j).|))))) are_congruent_mod ( Px (a, |.i.|)) by Th30;

      ((( - 1) * (( sgn ((2 * i) + j)) * ( Py (a, |.((2 * i) + j).|)))),(( - 1) * ( - (( sgn j) * ( Py (a, |.j.|)))))) are_congruent_mod ( Px (a, |.i.|)) by Th30, INT_4: 11;

      hence thesis by A1, INT_1: 15;

    end;

    theorem :: HILB10_1:28

    

     Th31: ((( sgn (((4 * x) * n) + y)) * ( Py (a, |.(((4 * x) * n) + y).|))),(( sgn y) * ( Py (a, |.y.|)))) are_congruent_mod ( Px (a, |.x.|))

    proof

      defpred P[ Nat] means ((( sgn (((4 * x) * $1) + y)) * ( Py (a, |.(((4 * x) * $1) + y).|))),(( sgn y) * ( Py (a, |.y.|)))) are_congruent_mod ( Px (a, |.x.|));

      

       A1: P[ 0 ] by INT_1: 11;

      

       A2: for n holds P[n] implies P[(n + 1)]

      proof

        let n;

        set n1 = (n + 1);

        assume

         A3: P[n];

        (((4 * x) * n1) + y) = ((4 * x) + (((4 * x) * n) + y));

        then ((( sgn (((4 * x) * n1) + y)) * ( Py (a, |.(((4 * x) * n1) + y).|))),(( sgn (((4 * x) * n) + y)) * ( Py (a, |.(((4 * x) * n) + y).|)))) are_congruent_mod ( Px (a, |.x.|)) by Lm7;

        hence thesis by A3, INT_1: 15;

      end;

      for n holds P[n] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    theorem :: HILB10_1:29

    

     Th32: ((( sgn (x + y)) * ( Py (a, |.(x + y).|))),(( sgn (x - y)) * ( Py (a, |.(x - y).|)))) are_congruent_mod ( Px (a, |.x.|))

    proof

      (x + y) = ((2 * x) + (( - x) + y));

      then

       A1: ((( sgn (x + y)) * ( Py (a, |.(x + y).|))),( - (( sgn (( - x) + y)) * ( Py (a, |.(( - x) + y).|))))) are_congruent_mod ( Px (a, |.x.|)) by Th30;

      

       A2: |.(( - x) + y).| = |.( - (( - x) + y)).| by COMPLEX1: 52;

      (( - x) + y) = (( - 1) * (x - y));

      then ( sgn (( - x) + y)) = (( sgn (x - y)) * ( sgn ( - 1))) & ( sgn ( - 1)) = ( - 1) by ABSVALUE: 18, ABSVALUE:def 2;

      hence thesis by A2, A1;

    end;

    

     Lm8: |.r1.| < r2 implies ( - r2) < r1 < r2

    proof

      assume

       A1: |.r1.| < r2;

      then

       A2: ( - |.r1.|) > ( - r2) by XREAL_1: 24;

      ( - |.r1.|) <= r1 <= |.r1.| by ABSVALUE: 4;

      hence thesis by A1, A2, XXREAL_0: 2;

    end;

    theorem :: HILB10_1:30

    

     Th33: n1 < n2 <= n & |.x.| = ( Py (a,n1)) & |.y.| = ( Py (a,n2)) & (x,y) are_congruent_mod ( Px (a,n)) implies x = y

    proof

      assume

       A1: n1 < n2 <= n & |.x.| = ( Py (a,n1)) & |.y.| = ( Py (a,n2)) & (x,y) are_congruent_mod ( Px (a,n));

      then

      consider i be Integer such that

       A2: (x - y) = (( Px (a,n)) * i) by INT_1:def 5;

      

       A3: n1 < n by A1, XXREAL_0: 2;

      ( - ( Px (a,n))) < (x - y) < ( Px (a,n))

      proof

        per cases ;

          suppose

           A4: a = 2;

          

           A5: (( sqrt 3) ^2 ) = 3 by SQUARE_1:def 2;

          

           A6: ( sqrt 3) > 0 by SQUARE_1: 25;

          ((3 + (2 * ( sqrt 3))) * ( Py (a,n1))) < ( Px (a,n)) by A4, A3, Th19;

          then ( Py (a,n1)) < (( Px (a,n)) / (3 + (2 * ( sqrt 3)))) by A6, XREAL_1: 81;

          then

           A7: ( - (( Px (a,n)) / (3 + (2 * ( sqrt 3))))) < x < (( Px (a,n)) / (3 + (2 * ( sqrt 3)))) by Lm8, A1;

          (( sqrt 3) * ( Py (a,n2))) < ( Px (a,n)) by A4, Th18, A1;

          then ( Py (a,n2)) < (( Px (a,n)) / ( sqrt 3)) by XREAL_1: 81, A6;

          then ( - (( Px (a,n)) / ( sqrt 3))) < y < (( Px (a,n)) / ( sqrt 3)) by Lm8, A1;

          then

           A8: (( - (( Px (a,n)) / (3 + (2 * ( sqrt 3))))) - (( Px (a,n)) / ( sqrt 3))) < (x - y) < ((( Px (a,n)) / (3 + (2 * ( sqrt 3)))) - ( - (( Px (a,n)) / ( sqrt 3)))) by A7, XREAL_1: 14;

          

           A9: ((( Px (a,n)) / (3 + (2 * ( sqrt 3)))) + (( Px (a,n)) / ( sqrt 3))) = (((( Px (a,n)) * ( sqrt 3)) + (( Px (a,n)) * (3 + (2 * ( sqrt 3))))) / ((3 + (2 * ( sqrt 3))) * ( sqrt 3))) by XCMPLX_1: 116, A6

          .= ((( Px (a,n)) * (3 + (3 * ( sqrt 3)))) / ((3 + (2 * ( sqrt 3))) * ( sqrt 3)))

          .= (( Px (a,n)) * ((3 + (3 * ( sqrt 3))) / ((3 * ( sqrt 3)) + 6))) by A5, XCMPLX_1: 74;

          (3 + (3 * ( sqrt 3))) <= (6 + (3 * ( sqrt 3))) by XREAL_1: 7;

          then ((3 + (3 * ( sqrt 3))) / ((3 * ( sqrt 3)) + 6)) <= 1 by A6, XREAL_1: 183;

          then

           A10: (( Px (a,n)) * ((3 + (3 * ( sqrt 3))) / ((3 * ( sqrt 3)) + 6))) <= (( Px (a,n)) * 1) by XREAL_1: 64;

          then ( - ((( Px (a,n)) / (3 + (2 * ( sqrt 3)))) + (( Px (a,n)) / ( sqrt 3)))) >= ( - ( Px (a,n))) by A9, XREAL_1: 24;

          hence thesis by A10, A8, A9, XXREAL_0: 2;

        end;

          suppose

           A11: a <> 2;

          (2 * ( Py (a,n1))) < ( Px (a,n)) by A11, A3, Th17;

          then |.x.| < (( Px (a,n)) / 2) by A1, XREAL_1: 81;

          then

           A12: ( - (( Px (a,n)) / 2)) < x < (( Px (a,n)) / 2) by Lm8;

          (2 * ( Py (a,n2))) < ( Px (a,n)) by A11, Th17, A1;

          then |.y.| < (( Px (a,n)) / 2) by A1, XREAL_1: 81;

          then ( - (( Px (a,n)) / 2)) < y < (( Px (a,n)) / 2) by Lm8;

          then (( - (( Px (a,n)) / 2)) - (( Px (a,n)) / 2)) < (x - y) < ((( Px (a,n)) / 2) - ( - (( Px (a,n)) / 2))) by A12, XREAL_1: 14;

          hence thesis;

        end;

      end;

      then (( - 1) * ( Px (a,n))) < (( Px (a,n)) * i) < (1 * ( Px (a,n))) by A2;

      then ( - 1) < i < (1 + 0 ) by XREAL_1: 64;

      then 0 <= i <= 0 by INT_1: 7, INT_1: 8;

      then (x - y) = 0 by A2;

      hence thesis;

    end;

    

     Lm9: n1 < n2 <= (2 * n) & |.x.| = ( Py (a,n1)) & |.y.| = ( Py (a,n2)) & (x,y) are_congruent_mod ( Px (a,n)) implies n1 = ((2 * n) - n2)

    proof

      assume

       A1: n1 < n2 <= (2 * n) & |.x.| = ( Py (a,n1)) & |.y.| = ( Py (a,n2)) & (x,y) are_congruent_mod ( Px (a,n)) & n1 <> ((2 * n) - n2);

      per cases ;

        suppose n2 <= n;

        then ( Py (a,n1)) = ( Py (a,n2)) by A1, Th33;

        hence thesis by A1, Th15;

      end;

        suppose

         A2: n2 > n;

        then

        reconsider m = (n2 - n) as Nat by NAT_1: 21;

        ((n + n) - n2) >= (n2 - n2) by A1, XREAL_1: 9;

        then

        reconsider nm = (n - m) as Element of NAT by INT_1: 3;

        

         A3: (( sgn n2) * ( Py (a, |.n2.|))) = ( Py (a,n2)) & (( sgn nm) * ( Py (a, |.nm.|))) = ( Py (a,nm)) by Th23;

        n2 = (n + m);

        then ((( sgn n2) * ( Py (a, |.n2.|))),(( sgn nm) * ( Py (a, |.nm.|)))) are_congruent_mod ( Px (a, |.n.|)) by Th32;

        then ((( sgn y) * ( Py (a,n2))),(( sgn y) * ( Py (a,nm)))) are_congruent_mod ( Px (a,n)) by A3, INT_4: 11;

        then (y,(( sgn y) * ( Py (a,nm)))) are_congruent_mod ( Px (a,n)) by A1, ABSVALUE: 17;

        then

         A4: (x,(( sgn y) * ( Py (a,nm)))) are_congruent_mod ( Px (a,n)) by A1, INT_1: 15;

        then

         A5: ((( sgn y) * ( Py (a,nm))),x) are_congruent_mod ( Px (a,n)) by INT_1: 14;

        nm = ((n + n) - n2);

        then

         A6: nm < ((n + n) - n) by A2, XREAL_1: 15;

        

         A7: n1 < nm or nm < n1 by A1, XXREAL_0: 1;

        y <> 0 by A1;

        then y > 0 or y < 0 ;

        then ( sgn y) = 1 or ( sgn y) = ( - 1) by ABSVALUE:def 2;

        then (( sgn y) * ( Py (a,nm))) = ( Py (a,nm)) or (( sgn y) * ( Py (a,nm))) = ( - ( Py (a,nm)));

        then

         A8: |.(( sgn y) * ( Py (a,nm))).| = ( Py (a,nm));

        per cases ;

          suppose n1 <= n;

          then

           A9: ( Py (a,n1)) = ( Py (a,nm)) or ( Py (a,n1)) = ( - ( Py (a,nm))) by A1, A4, INT_1: 14, A8, A6, A7, Th33;

          ( Py (a,n1)) <> ( - ( Py (a,nm)))

          proof

            assume

             A10: ( Py (a,n1)) = ( - ( Py (a,nm)));

            n1 = 0 & nm = 0 by A10;

            hence thesis by A1;

          end;

          hence thesis by A9, A1, Th15;

        end;

          suppose

           A11: n1 > n;

          then

          reconsider k = (n1 - n) as Nat by NAT_1: 21;

          (n + n) >= n1 by A1, XXREAL_0: 2;

          then ((n + n) - n1) >= (n1 - n1) by XREAL_1: 9;

          then

          reconsider nk = (n - k) as Element of NAT by INT_1: 3;

          

           A12: (( sgn n1) * ( Py (a, |.n1.|))) = ( Py (a,n1)) & (( sgn nk) * ( Py (a, |.nk.|))) = ( Py (a,nk)) by Th23;

          n1 = (n + k);

          then ((( sgn n1) * ( Py (a, |.n1.|))),(( sgn nk) * ( Py (a, |.nk.|)))) are_congruent_mod ( Px (a, |.n.|)) by Th32;

          then ((( sgn x) * ( Py (a,n1))),(( sgn x) * ( Py (a,nk)))) are_congruent_mod ( Px (a,n)) by A12, INT_4: 11;

          then (x,(( sgn x) * ( Py (a,nk)))) are_congruent_mod ( Px (a,n)) by A1, ABSVALUE: 17;

          then

           A13: ((( sgn y) * ( Py (a,nm))),(( sgn x) * ( Py (a,nk)))) are_congruent_mod ( Px (a,n)) by A5, INT_1: 15;

          nk = ((n + n) - n1);

          then

           A14: nk < ((n + n) - n) by A11, XREAL_1: 15;

          

           A15: nk <> nm by A1;

          then

           A16: nk < nm or nm < nk by XXREAL_0: 1;

          x <> 0 by A1, A11;

          then x > 0 or x < 0 ;

          then ( sgn x) = 1 or ( sgn x) = ( - 1) by ABSVALUE:def 2;

          then (( sgn x) * ( Py (a,nk))) = ( Py (a,nk)) or (( sgn x) * ( Py (a,nk))) = ( - ( Py (a,nk)));

          then

           A17: |.(( sgn x) * ( Py (a,nk))).| = ( Py (a,nk));

          

           A18: ( Py (a,nk)) = ( Py (a,nm)) or ( Py (a,nk)) = ( - ( Py (a,nm))) by Th33, A16, A14, A6, A13, INT_1: 14, A8, A17;

          ( Py (a,nk)) <> ( - ( Py (a,nm)))

          proof

            assume

             A19: ( Py (a,nk)) = ( - ( Py (a,nm)));

            nk = 0 & nm = 0 by A19;

            hence thesis by A1;

          end;

          hence thesis by A18, A15, Th15;

        end;

      end;

    end;

    theorem :: HILB10_1:31

    

     Th34: n1 <= (2 * n) & n2 <= (2 * n) & |.x.| = ( Py (a,n1)) & |.y.| = ( Py (a,n2)) & (x,y) are_congruent_mod ( Px (a,n)) implies (n1,n2) are_congruent_mod (2 * n) or (n1,( - n2)) are_congruent_mod (2 * n)

    proof

      assume that

       A1: n1 <= (2 * n) & n2 <= (2 * n) and

       A2: |.x.| = ( Py (a,n1)) & |.y.| = ( Py (a,n2)) & (x,y) are_congruent_mod ( Px (a,n));

      n1 = n2 or n1 > n2 or n1 < n2 by XXREAL_0: 1;

      then n1 = n2 or n1 = ((2 * n) - n2) or n2 = ((2 * n) - n1) by Lm9, A2, INT_1: 14, A1;

      then (n1 - n2) = ((2 * n) * 0 ) or (n1 - ( - n2)) = ((2 * n) * 1) or (n1 - ( - n2)) = ((2 * n) * ( - 1));

      hence thesis by INT_1:def 5;

    end;

    

     Lm10: n1 <= (2 * n) & (2 * n) < n2 <= (4 * n) & |.x.| = ( Py (a,n1)) & |.y.| = ( Py (a,n2)) & (x,y) are_congruent_mod ( Px (a,n)) implies (n1,n2) are_congruent_mod (2 * n) or (n1,( - n2)) are_congruent_mod (2 * n)

    proof

      assume that

       A1: n1 <= (2 * n) & (2 * n) < n2 <= (4 * n) and

       A2: |.x.| = ( Py (a,n1)) & |.y.| = ( Py (a,n2)) & (x,y) are_congruent_mod ( Px (a,n));

      reconsider m1 = (n2 - (2 * n)) as Nat by A1, NAT_1: 21;

      

       A3: m1 <= ((4 * n) - (2 * n)) by A1, XREAL_1: 9;

      m1 > ((2 * n) - (2 * n)) & n2 > 0 by XREAL_1: 9, A1;

      then

       A4: ( sgn m1) = 1 & ( sgn n2) = 1 by ABSVALUE:def 2;

      y <> 0 by A2, A1;

      then y > 0 or y < 0 ;

      then ( sgn y) = 1 or ( sgn y) = ( - 1) by ABSVALUE:def 2;

      then

       A5: |.(( sgn y) * ( - ( Py (a,m1)))).| = ( Py (a,m1));

      ((2 * n) + m1) = n2;

      then ((( sgn n2) * ( Py (a, |.n2.|))),( - (( sgn m1) * ( Py (a, |.m1.|))))) are_congruent_mod ( Px (a, |.n.|)) by Th30;

      then ((( sgn y) * ( Py (a, |.n2.|))),(( sgn y) * ( - ( Py (a,m1))))) are_congruent_mod ( Px (a,n)) by A4, INT_4: 11;

      then (y,(( sgn y) * ( - ( Py (a,m1))))) are_congruent_mod ( Px (a,n)) by ABSVALUE: 17, A2;

      then

       A6: (x,(( sgn y) * ( - ( Py (a,m1))))) are_congruent_mod ( Px (a,n)) by INT_1: 15, A2;

      per cases by XXREAL_0: 1;

        suppose n1 < m1 or n1 > m1;

        then n1 = ((2 * n) - m1) or m1 = ((2 * n) - n1) by A6, INT_1: 14, A1, A2, A5, A3, Lm9;

        then (n1 - ( - n2)) = (2 * (2 * n));

        hence thesis by INT_1:def 5;

      end;

        suppose n1 = m1;

        then (n1 - n2) = (( - 1) * (2 * n));

        hence thesis by INT_1:def 5;

      end;

    end;

    

     Lm11: (2 * n) < n1 <= (4 * n) & (2 * n) < n2 <= (4 * n) & |.x.| = ( Py (a,n1)) & |.y.| = ( Py (a,n2)) & (x,y) are_congruent_mod ( Px (a,n)) implies (n1,n2) are_congruent_mod (2 * n) or (n1,( - n2)) are_congruent_mod (2 * n)

    proof

      assume that

       A1: (2 * n) < n1 <= (4 * n) & (2 * n) < n2 <= (4 * n) and

       A2: |.x.| = ( Py (a,n1)) & |.y.| = ( Py (a,n2)) & (x,y) are_congruent_mod ( Px (a,n));

      reconsider m2 = (n2 - (2 * n)) as Nat by A1, NAT_1: 21;

      

       A3: m2 <= ((4 * n) - (2 * n)) by A1, XREAL_1: 9;

      m2 > ((2 * n) - (2 * n)) & n2 > 0 by XREAL_1: 9, A1;

      then

       A4: ( sgn m2) = 1 & ( sgn n2) = 1 by ABSVALUE:def 2;

      y <> 0 by A2, A1;

      then y > 0 or y < 0 ;

      then ( sgn y) = 1 or ( sgn y) = ( - 1) by ABSVALUE:def 2;

      then

       A5: |.(( sgn y) * ( - ( Py (a,m2)))).| = ( Py (a,m2));

      reconsider m1 = (n1 - (2 * n)) as Nat by A1, NAT_1: 21;

      

       A6: m1 <= ((4 * n) - (2 * n)) by A1, XREAL_1: 9;

      m1 > ((2 * n) - (2 * n)) & n1 > 0 by XREAL_1: 9, A1;

      then

       A7: ( sgn m1) = 1 & ( sgn n1) = 1 by ABSVALUE:def 2;

      x <> 0 by A2, A1;

      then x > 0 or x < 0 ;

      then ( sgn x) = 1 or ( sgn x) = ( - 1) by ABSVALUE:def 2;

      then

       A8: |.(( sgn x) * ( - ( Py (a,m1)))).| = ( Py (a,m1));

      ((2 * n) + m1) = n1;

      then ((( sgn n1) * ( Py (a, |.n1.|))),( - (( sgn m1) * ( Py (a, |.m1.|))))) are_congruent_mod ( Px (a, |.n.|)) by Th30;

      then ((( sgn x) * ( Py (a, |.n1.|))),(( sgn x) * ( - ( Py (a,m1))))) are_congruent_mod ( Px (a,n)) by A7, INT_4: 11;

      then (x,(( sgn x) * ( - ( Py (a,m1))))) are_congruent_mod ( Px (a,n)) by ABSVALUE: 17, A2;

      then ((( sgn x) * ( - ( Py (a,m1)))),x) are_congruent_mod ( Px (a,n)) by INT_1: 14;

      then

       A9: ((( sgn x) * ( - ( Py (a,m1)))),y) are_congruent_mod ( Px (a,n)) by INT_1: 15, A2;

      ((2 * n) + m2) = n2;

      then ((( sgn n2) * ( Py (a, |.n2.|))),( - (( sgn m2) * ( Py (a, |.m2.|))))) are_congruent_mod ( Px (a, |.n.|)) by Th30;

      then ((( sgn y) * ( Py (a, |.n2.|))),(( sgn y) * ( - ( Py (a,m2))))) are_congruent_mod ( Px (a,n)) by A4, INT_4: 11;

      then (y,(( sgn y) * ( - ( Py (a,m2))))) are_congruent_mod ( Px (a,n)) by ABSVALUE: 17, A2;

      then

       A10: ((( sgn x) * ( - ( Py (a,m1)))),(( sgn y) * ( - ( Py (a,m2))))) are_congruent_mod ( Px (a,n)) by A9, INT_1: 15;

      per cases by XXREAL_0: 1;

        suppose m1 < m2 or m1 > m2;

        then m1 = ((2 * n) - m2) or m2 = ((2 * n) - m1) by A10, INT_1: 14, A5, A3, A6, A8, Lm9;

        then (n1 - ( - n2)) = (3 * (2 * n));

        hence thesis by INT_1:def 5;

      end;

        suppose m1 = m2;

        then (n1 - n2) = ( 0 * (2 * n));

        hence thesis by INT_1:def 5;

      end;

    end;

    theorem :: HILB10_1:32

    

     Th35: n1 <= (4 * n) & n2 <= (4 * n) & |.x.| = ( Py (a,n1)) & |.y.| = ( Py (a,n2)) & (x,y) are_congruent_mod ( Px (a,n)) implies (n1,n2) are_congruent_mod (2 * n) or (n1,( - n2)) are_congruent_mod (2 * n)

    proof

      assume

       A1: n1 <= (4 * n) & n2 <= (4 * n) & |.x.| = ( Py (a,n1)) & |.y.| = ( Py (a,n2)) & (x,y) are_congruent_mod ( Px (a,n));

      then

       A2: (y,x) are_congruent_mod ( Px (a,n)) by INT_1: 14;

      per cases ;

        suppose n1 <= (2 * n) & n2 <= (2 * n) or n1 > (2 * n) & n2 > (2 * n) or n1 <= (2 * n) < n2;

        hence thesis by A1, Th34, Lm10, Lm11;

      end;

        suppose n2 <= (2 * n) < n1;

        then (n2,n1) are_congruent_mod (2 * n) or (n2,( - n1)) are_congruent_mod (2 * n) by A1, A2, Lm10;

        then (n1,n2) are_congruent_mod (2 * n) or ((( - 1) * n2),(( - 1) * ( - n1))) are_congruent_mod (2 * n) by INT_1: 14, INT_4: 11;

        hence thesis by INT_1: 14;

      end;

    end;

    theorem :: HILB10_1:33

    

     Th36: (( Py (a,n1)),( Py (a,n2))) are_congruent_mod ( Px (a,n)) & n > 0 implies (n1,n2) are_congruent_mod (2 * n) or (n1,( - n2)) are_congruent_mod (2 * n)

    proof

      assume that

       A1: (( Py (a,n1)),( Py (a,n2))) are_congruent_mod ( Px (a,n)) and

       A2: n > 0 ;

      reconsider m1 = (n1 mod (4 * n)), d1 = (n1 div (4 * n)) as Element of NAT ;

      

       A3: (n1 - (d1 * (4 * n))) = m1 by A2, INT_1:def 10;

      then ((( sgn (((4 * d1) * n) + m1)) * ( Py (a, |.(((4 * d1) * n) + m1).|))),(( sgn m1) * ( Py (a, |.m1.|)))) are_congruent_mod ( Px (a, |.n.|)) by Th31;

      then (( Py (a,n1)),(( sgn m1) * ( Py (a, |.m1.|)))) are_congruent_mod ( Px (a, |.n.|)) by A3, Th23;

      then (( Py (a,n1)),( Py (a,m1))) are_congruent_mod ( Px (a,n)) by Th23;

      then

       A4: (( Py (a,m1)),( Py (a,n1))) are_congruent_mod ( Px (a,n)) by INT_1: 14;

      reconsider m2 = (n2 mod (4 * n)), d2 = (n2 div (4 * n)) as Element of NAT ;

      

       A5: m1 <= (4 * n) & m2 <= (4 * n) by A2, INT_1: 58;

      

       A6: |.( Py (a,m1)).| = ( Py (a,m1)) & |.( Py (a,m2)).| = ( Py (a,m2));

      

       A7: (n2 - (d2 * (4 * n))) = m2 by A2, INT_1:def 10;

      then ((( sgn (((4 * d2) * n) + m2)) * ( Py (a, |.(((4 * d2) * n) + m2).|))),(( sgn m2) * ( Py (a, |.m2.|)))) are_congruent_mod ( Px (a, |.n.|)) by Th31;

      then (( Py (a,n2)),(( sgn m2) * ( Py (a, |.m2.|)))) are_congruent_mod ( Px (a, |.n.|)) by A7, Th23;

      then (( Py (a,n2)),( Py (a,m2))) are_congruent_mod ( Px (a,n)) by Th23;

      then (( Py (a,n1)),( Py (a,m2))) are_congruent_mod ( Px (a,n)) by A1, INT_1: 15;

      then (( Py (a,m1)),( Py (a,m2))) are_congruent_mod ( Px (a,n)) by A4, INT_1: 15;

      then

       A8: (m1,m2) are_congruent_mod (2 * n) or (m1,( - m2)) are_congruent_mod (2 * n) by A6, A5, Th35;

      (n1 - m1) = ((2 * d1) * (2 * n)) by A3;

      then (n1,m1) are_congruent_mod (2 * n) by INT_1:def 5;

      then

       A9: (n1,m2) are_congruent_mod (2 * n) or (n1,( - m2)) are_congruent_mod (2 * n) by A8, INT_1: 15;

      (m2 - n2) = (( - (2 * d2)) * (2 * n)) & (( - m2) - ( - n2)) = ((2 * d2) * (2 * n)) by A7;

      then (m2,n2) are_congruent_mod (2 * n) & (( - m2),( - n2)) are_congruent_mod (2 * n) by INT_1:def 5;

      hence thesis by A9, INT_1: 15;

    end;

    begin

    theorem :: HILB10_1:34

    

     Th37: ( Py (a,n)) divides ( Py (a,(n * k)))

    proof

      defpred P[ Nat] means ( Py (a,n)) divides ( Py (a,(n * $1)));

      (( Py (a,n)) * 0 ) = ( Py (a,(n * 0 ))) by Th6;

      then

       A1: P[ 0 ] by INT_1:def 3;

      

       A2: for k holds P[k] implies P[(k + 1)]

      proof

        let k;

        assume

         A3: P[k];

        

         A4: ( Py (a,((n * k) + n))) = (( sgn ((n * k) + n)) * ( Py (a, |.((n * k) + n).|))) & (( sgn n) * ( Py (a, |.n.|))) = ( Py (a,n)) & (( sgn (n * k)) * ( Py (a, |.(n * k).|))) = ( Py (a,(n * k))) by Th23;

        

        then

         A5: ( Py (a, |.((n * k) + n).|)) = (((( Px (a, |.(n * k).|)) * ( sgn n)) * ( Py (a, |.n.|))) + ((( sgn (n * k)) * ( Py (a, |.(n * k).|))) * ( Px (a, |.n.|)))) by Th25

        .= ((( Px (a,(n * k))) * ( Py (a,n))) + (( Py (a,(n * k))) * ( Px (a,n)))) by A4;

        

         A6: ( Py (a,n)) divides (( Py (a,(n * k))) * ( Px (a,n))) by A3, INT_2: 2;

        ( Py (a,n)) divides (( Px (a,(n * k))) * ( Py (a,n))) by NAT_D: 9;

        hence thesis by A5, A6, NAT_D: 8;

      end;

      for k holds P[k] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    theorem :: HILB10_1:35

    

     Th38: (( Py (a,(n * k))),((k * (( Px (a,n)) |^ (k -' 1))) * ( Py (a,n)))) are_congruent_mod (( Py (a,n)) ^2 )

    proof

      set m = ( min_Pell's_solution_of ((a ^2 ) -' 1));

      set x = ( Px (a,n)), y = ( Py (a,n)), s = ( sqrt ((a ^2 ) -' 1)), ys = (y * s);

      per cases ;

        suppose n = 0 or k = 0 ;

        then (y = 0 or k = 0 ) & ( Py (a,(n * k))) = 0 by Th6;

        hence thesis by INT_1: 11;

      end;

        suppose

         A1: n > 0 & k > 0 ;

        set I = ((x,ys) In_Power k);

        

         A2: (x + ys) = (((m `1 ) + ((m `2 ) * s)) |^ n) by Def2;

        

         A3: (( Px (a,(n * k))) + (( Py (a,(n * k))) * s)) = (((m `1 ) + ((m `2 ) * s)) |^ (n * k)) by Def2

        .= ((x + ys) |^ k) by A2, NEWTON: 9

        .= ( Sum I) by NEWTON: 30;

        consider e,o be complex-valued FinSequence such that

         A4: ( len e) = [\(( len I) / 2)/] & ( len o) = [/(( len I) / 2)\] and

         A5: ( Sum I) = (( Sum e) + ( Sum o)) and

         A6: for n holds (e . n) = (I . (2 * n)) & (o . n) = (I . ((2 * n) - 1)) by Th2;

        

         A7: ( len I) = (k + 1) by NEWTON:def 4;

        (s |^ (1 + 1)) = (s * (s |^ 1)) by NEWTON: 6

        .= (s ^2 )

        .= ((a ^2 ) -' 1) by SQUARE_1:def 2;

        then

         A8: (ys |^ 2) = ((y |^ 2) * ((a ^2 ) -' 1)) by NEWTON: 7;

        ( rng o) c= NAT

        proof

          let w be object;

          assume w in ( rng o);

          then

          consider z be object such that

           A9: z in ( dom o) & (o . z) = w by FUNCT_1:def 3;

          reconsider z as Nat by A9;

          set Z = ((2 * z) - 1);

          

           A10: w = (I . Z) by A6, A9;

          

           A11: 1 <= z <= ( len o) by A9, FINSEQ_3: 25;

          

           A12: (2 * z) >= (2 * 1) by XREAL_1: 64, A9, FINSEQ_3: 25;

          then

           A13: Z >= (2 - 1) by XREAL_1: 9;

          reconsider zz = Z, m = (Z - 1) as Nat by A12;

          

           A14: ((( len I) / 2) + 1) = ((( len I) + 2) / 2);

          ( len o) < ((( len I) / 2) + 1) by A4, INT_1:def 7;

          then z < ((( len I) / 2) + 1) by A11, XXREAL_0: 2;

          then (2 * z) < ((k + 1) + 2) & ((k + 1) + 2) = ((k + 2) + 1) by A7, A14, XREAL_1: 79;

          then

           A15: (2 * z) <= ((k + 1) + 1) by NAT_1: 13;

          then

           A16: Z <= (k + 1) by XREAL_1: 20;

          reconsider l = ((k + 1) - zz) as Nat by NAT_1: 21, XREAL_1: 20, A15;

          

           A17: Z in ( dom I) by A16, A7, A13, FINSEQ_3: 25;

          l = (k - m);

          then

           A18: (I . Z) = (((k choose m) * (x |^ l)) * (ys |^ m)) by A17, NEWTON:def 4;

          reconsider z1 = (z - 1) as Nat by A11;

          m = (2 * z1);

          then (ys |^ m) = (((y |^ 2) * ((a ^2 ) -' 1)) |^ z1) by A8, NEWTON: 9;

          hence thesis by A10, A18, ORDINAL1:def 12;

        end;

        then

        reconsider o as FinSequence of NAT by FINSEQ_1:def 4;

        defpred E[ object, object] means $2 in NAT & for n be Nat st n = $2 holds (e . $1) = (s * n) & for N be Nat st N = $1 holds (N - 1) is Nat & ((2 * N) - 1) is Nat & ((k + 1) - (2 * N)) is Nat & for n1,m,l be Nat st n1 = (N - 1) & m = ((2 * N) - 1) & l = ((k + 1) - (2 * N)) holds $2 = (((k choose m) * (x |^ l)) * ((((y |^ 2) * ((a ^2 ) -' 1)) |^ n1) * y));

        

         A19: for n st n in ( Seg ( len e)) holds ex x be object st E[n, x]

        proof

          let n such that

           A20: n in ( Seg ( len e));

          set N = (2 * n);

          

           A21: 1 <= n <= ( len e) by A20, FINSEQ_1: 1;

          then N >= (2 * 1) by XREAL_1: 64;

          then

           A22: N >= 1 by XXREAL_0: 2;

          reconsider m = (N - 1), n1 = (n - 1) as Nat by A21;

          ( len e) <= (( len I) / 2) by A4, INT_1:def 6;

          then n <= (( len I) / 2) by A21, XXREAL_0: 2;

          then

           A23: N <= (k + 1) by A7, XREAL_1: 83;

          then

          reconsider l = ((k + 1) - N) as Nat by NAT_1: 21;

          take U = (((k choose m) * (x |^ l)) * ((((y |^ 2) * ((a ^2 ) -' 1)) |^ n1) * y));

          thus U in NAT by ORDINAL1:def 12;

          let u be Nat such that

           A24: u = U;

          

           A25: N in ( dom I) by A23, A7, A22, FINSEQ_3: 25;

          l = (k - m);

          then

           A26: (I . N) = (((k choose m) * (x |^ l)) * (ys |^ m)) by A25, NEWTON:def 4;

          m = ((2 * n1) + 1);

          

          then (ys |^ m) = ((ys |^ (2 * n1)) * ys) by NEWTON: 6

          .= ((((y |^ 2) * ((a ^2 ) -' 1)) |^ n1) * ys) by A8, NEWTON: 9;

          hence (e . n) = (s * u) by A6, A26, A24;

          let nn be Nat such that

           A27: n = nn;

          (nn - 1) = n1 & ((2 * nn) - 1) = m & ((k + 1) - (2 * nn)) = l by A27;

          hence thesis;

        end;

        consider p be FinSequence such that

         A28: ( dom p) = ( Seg ( len e)) & for n st n in ( Seg ( len e)) holds E[n, (p . n)] from FINSEQ_1:sch 1( A19);

        ( rng p) c= NAT

        proof

          let w be object;

          assume w in ( rng p);

          then ex n be object st n in ( dom p) & (p . n) = w by FUNCT_1:def 3;

          hence thesis by A28;

        end;

        then

        reconsider p as FinSequence of NAT by FINSEQ_1:def 4;

        

         A29: ( dom (s * p)) = ( dom p) & ( dom p) = ( dom e) by A28, VALUED_1:def 5, FINSEQ_1:def 3;

        

         A30: ( len p) = ( len e) by A28, FINSEQ_1:def 3;

        for n st n in ( dom p) holds (e . n) = ((s * p) . n)

        proof

          let n;

          assume n in ( dom p);

          

          hence (e . n) = (s * (p . n)) by A28

          .= ((s * p) . n) by VALUED_1: 6;

        end;

        then e = (s * p) by A29, FINSEQ_1: 13;

        then ( Sum I) = (( Sum o) + (s * ( Sum p))) by A5, RVSUM_1: 87;

        then

         A31: ( Py (a,(n * k))) = ( Sum p) by A3, PELLS_EQ: 3;

        

         A32: ( Sum p) is Nat by TARSKI: 1;

        

         A33: (y |^ (1 + 1)) = (y * (y |^ 1)) by NEWTON: 6

        .= (y * y);

        for n st 1 < n <= ( len p) holds ((p . n) mod (y ^2 )) = 0

        proof

          let n;

          assume

           A34: 1 < n <= ( len p);

          then

           A35: n in ( Seg ( len e)) by A28, FINSEQ_3: 25;

          then E[n, (p . n)] by A28;

          then

          reconsider n1 = (n - 1), m = ((2 * n) - 1), l = ((k + 1) - (2 * n)) as Nat;

          

           A36: (p . n) = (((k choose m) * (x |^ l)) * ((((y |^ 2) * ((a ^2 ) -' 1)) |^ n1) * y)) by A35, A28;

          

           A37: (n - 1) > (1 - 1) by A34, XREAL_1: 9;

          (y ^2 ) divides (((y |^ 2) * ((a ^2 ) -' 1)) |^ n1) by A37, NEWTON02: 14, A33, INT_1:def 3;

          then (y ^2 ) divides ((((y |^ 2) * ((a ^2 ) -' 1)) |^ n1) * y) by NAT_D: 9;

          then (y ^2 ) divides (p . n) by A36, NAT_D: 9;

          hence thesis by INT_1: 62, A1;

        end;

        then (( Sum p) mod (y ^2 )) = ((p . 1) mod (y ^2 )) by Th1;

        then ((( Sum p) - (p . 1)) mod (y ^2 )) = 0 by A32, INT_4: 22, A1;

        then (y ^2 ) divides (( Sum p) - (p . 1)) by INT_1: 62, A1;

        then

         A38: (( Sum p),(p . 1)) are_congruent_mod (y ^2 ) by INT_1:def 4;

        ( len I) >= (1 + 1) & (1 + 1) = (2 * 1) by XREAL_1: 6, A7, A1, NAT_1: 14;

        then (( len I) / 2) >= 1 by XREAL_1: 77;

        then ( len p) >= 1 by INT_1: 54, A30, A4;

        then

         A39: 1 in ( Seg ( len e)) by A28, FINSEQ_3: 25;

        then E[1, (p . 1)] by A28;

        then

        reconsider l = ((k + 1) - (2 * 1)) as Nat;

        

         A40: (k choose 1) = k by NEWTON: 23, A1, NAT_1: 14;

        

         A41: (((y |^ 2) * ((a ^2 ) -' 1)) |^ 0 ) = 1 by NEWTON: 4;

        

         A42: l = (k - 1);

        (1 - 1) = 0 & ((2 * 1) - 1) = 1;

        then (p . 1) = ((k * (x |^ l)) * (1 * y)) by A39, A28, A40, A41;

        hence thesis by A42, A31, A38, XREAL_0:def 2;

      end;

    end;

    theorem :: HILB10_1:36

    

     Th39: k > 0 & ( Py (a,k)) divides ( Py (a,n)) implies k divides n

    proof

      set Pk = ( Py (a,k)), Pn = ( Py (a,n));

      set r = (n mod k), q = (n div k);

      assume

       A1: k > 0 & Pk divides Pn;

      reconsider r, q as Element of NAT ;

      

       A2: r = (n - (q * k)) by A1, INT_1:def 10;

      then n = (r + (q * k));

      then (( sgn n) * ( Py (a, |.n.|))) = (((( Px (a, |.r.|)) * ( sgn (q * k))) * ( Py (a, |.(q * k).|))) + ((( sgn r) * ( Py (a, |.r.|))) * ( Px (a, |.(q * k).|)))) by Th25;

      

      then

       A3: ( Py (a,n)) = ((( Px (a, |.r.|)) * (( sgn (q * k)) * ( Py (a, |.(q * k).|)))) + ((( sgn r) * ( Py (a, |.r.|))) * ( Px (a, |.(q * k).|)))) by Th23

      .= ((( Px (a, |.r.|)) * ( Py (a,(q * k)))) + ((( sgn r) * ( Py (a, |.r.|))) * ( Px (a, |.(q * k).|)))) by Th23

      .= ((( Px (a,r)) * ( Py (a,(q * k)))) + (( Py (a,r)) * ( Px (a,(q * k))))) by Th23;

      

       A4: Pk divides ( Py (a,(q * k))) by Th37;

      Pk divides (( Px (a,r)) * ( Py (a,(q * k)))) by Th37, INT_2: 2;

      then

       A5: Pk divides (( Py (a,r)) * ( Px (a,(q * k)))) by INT_2: 1, A1, A3;

      

       A6: (Pk,( Px (a,(k * q)))) are_coprime

      proof

        (Pk gcd ( Px (a,(k * q)))) divides ( Py (a,k)) by INT_2:def 2;

        then

         A7: (( Py (a,k)) gcd ( Px (a,(k * q)))) divides ( Py (a,(q * k))) by A4, INT_2: 9;

        (Pk gcd ( Px (a,(k * q)))) divides ( Px (a,(k * q))) by INT_2:def 2;

        then (Pk gcd ( Px (a,(k * q)))) divides (( Py (a,(q * k))) gcd ( Px (a,(k * q)))) by A7, INT_2: 22;

        then (Pk gcd ( Px (a,(k * q)))) divides 1 by Th26, INT_2:def 3;

        then (Pk gcd ( Px (a,(k * q)))) = 1 by INT_2: 13;

        hence thesis by INT_2:def 3;

      end;

      r = 0

      proof

        assume r <> 0 ;

        then |.Pk.| <= |.( Py (a,r)).| by A6, INT_4: 6, A5, INT_2: 25;

        hence thesis by Th14, INT_1: 58, A1;

      end;

      hence thesis by A2, INT_1:def 3;

    end;

    theorem :: HILB10_1:37

    

     Th40: (( Py (a,k)) ^2 ) divides ( Py (a,n)) implies ( Py (a,k)) divides n

    proof

      assume

       A1: (( Py (a,k)) ^2 ) divides ( Py (a,n));

      per cases ;

        suppose k = 0 ;

        then ( Py (a,k)) = 0 by Th6;

        then ex i be Integer st ( 0 * i) = ( Py (a,n)) by A1, INT_1:def 3;

        then (( Py (a,k)) * 0 ) = n;

        hence thesis by INT_1:def 3;

      end;

        suppose

         A2: k > 0 ;

        ( Py (a,k)) divides (( Py (a,k)) ^2 ) by INT_1:def 3;

        then ( Py (a,k)) divides ( Py (a,n)) by A1, INT_2: 9;

        then

        consider w be Nat such that

         A3: (k * w) = n by NAT_D:def 3, Th39, A2;

        

         A4: w divides n by A3, NAT_D:def 3;

        (( Py (a,k)) ^2 ) divides (( Py (a,n)) - 0 ) by A1;

        then

         A5: ( 0 ,( Py (a,n))) are_congruent_mod (( Py (a,k)) ^2 ) by INT_1: 14, INT_1:def 4;

        (( Py (a,n)),((w * (( Px (a,k)) |^ (w -' 1))) * ( Py (a,k)))) are_congruent_mod (( Py (a,k)) ^2 ) by Th38, A3;

        then

         A6: (( 0 * (( Px (a,k)) |^ (w -' 1))),((w * ( Py (a,k))) * (( Px (a,k)) |^ (w -' 1)))) are_congruent_mod (( Py (a,k)) ^2 ) by A5, INT_1: 15;

        

         A7: ( Py (a,k)) in NAT & w in NAT by ORDINAL1:def 12;

        

         A8: (( Py (a,k)) ^2 ) = (( Py (a,k)) * (( Py (a,k)) |^ 1))

        .= (( Py (a,k)) |^ (1 + 1)) by NEWTON: 6;

        (( Py (a,k)),( Px (a,k))) are_coprime by Th26;

        then ((( Py (a,k)) |^ 2),( Px (a,k))) are_coprime by WSIERP_1: 10;

        then ( 0 ,(w * ( Py (a,k)))) are_congruent_mod (( Py (a,k)) ^2 ) by A6, A8, INT_4: 9, WSIERP_1: 10;

        then (( Py (a,k)) ^2 ) divides ((w * ( Py (a,k))) - 0 ) by INT_1:def 4, INT_1: 14;

        then ( Py (a,k)) divides w or ( Py (a,k)) = 0 by A7, PYTHTRIP: 7;

        hence thesis by A4, A2, INT_2: 9;

      end;

    end;

    begin

    theorem :: HILB10_1:38

    for y,z,a be Nat holds y = ( Py (a,z)) & a > 1 iff ex x,x1,y1,A,x2,y2 be Nat st a > 1 & [x, y] is Pell's_solution of ((a ^2 ) -' 1) & [x1, y1] is Pell's_solution of ((a ^2 ) -' 1) & y1 >= y & A > y & y >= z & [x2, y2] is Pell's_solution of ((A ^2 ) -' 1) & (y2,y) are_congruent_mod x1 & (A,a) are_congruent_mod x1 & (y2,z) are_congruent_mod (2 * y) & (A,1) are_congruent_mod (2 * y) & (y1, 0 ) are_congruent_mod (y ^2 )

    proof

      let y,z,a be Nat;

      thus y = ( Py (a,z)) & a > 1 implies ex x,x1,y1,A,x2,y2 be Nat st a > 1 & [x, y] is Pell's_solution of ((a ^2 ) -' 1) & [x1, y1] is Pell's_solution of ((a ^2 ) -' 1) & y1 >= y & A > y & y >= z & [x2, y2] is Pell's_solution of ((A ^2 ) -' 1) & (y2,y) are_congruent_mod x1 & (A,a) are_congruent_mod x1 & (y2,z) are_congruent_mod (2 * y) & (A,1) are_congruent_mod (2 * y) & (y1, 0 ) are_congruent_mod (y ^2 )

      proof

        assume

         A1: y = ( Py (a,z)) & a > 1;

        then

         A2: a is non trivial by NAT_2: 28;

        set x = ( Px (a,z));

        

         A3: a >= (1 + 1) by NAT_1: 13, A1;

        

         A4: ((a ^2 ) -' 1) = ((a ^2 ) - 1) by XREAL_1: 233, NAT_1: 14, A1;

        ((x ^2 ) - (((a ^2 ) -' 1) * (y ^2 ))) = 1 by A1, Th10, A2;

        then

         A5: [x, y] is Pell's_solution of ((a ^2 ) -' 1) & a > 1 by A1, Lm3;

        

         A6: y >= z by Th16, A1, A2;

        per cases ;

          suppose

           A7: y = 0 ;

          then

           A8: z = 0 by A1, A2;

          then

           A9: x = 1 by Th6, A2;

          set x1 = x, y1 = y, y2 = y, A = 1;

          ((A ^2 ) -' 1) = (1 - 1) by XREAL_1: 233;

          then

           A10: ((1 ^2 ) - (((A ^2 ) -' 1) * (y2 ^2 ))) = 1;

          1 in INT & 0 in INT by INT_1:def 2;

          then

           A11: [1, 0 ] in [: INT , INT :] by ZFMISC_1: 87;

          ( [1, 0 ] `1 ) = 1 & ( [1, 0 ] `2 ) = 0 ;

          then

           A12: [1, y2] is Pell's_solution of ((A ^2 ) -' 1) by A10, A11, A7, PELLS_EQ:def 1;

          

           A13: (y2,y) are_congruent_mod x1 by INT_1: 11;

          

           A14: (A,a) are_congruent_mod x1 by INT_1: 13, A9;

          

           A15: (A,1) are_congruent_mod (2 * y) by INT_1: 11;

          (y1, 0 ) are_congruent_mod (y ^2 ) by A7, INT_1: 11;

          hence thesis by A5, A12, A13, A14, A8, A7, A15;

        end;

          suppose

           A16: y > 0 ;

          reconsider B = (((a ^2 ) -' 1) * ((2 * (y ^2 )) ^2 )) as non square Nat by A2, A16;

          set M = ( min_Pell's_solution_of B);

          set x1 = (M `1 ), Y1 = (M `2 );

          

           A17: ((x1 ^2 ) - (B * (Y1 ^2 ))) = 1 by PELLS_EQ:def 1;

          set y1 = ((2 * (y ^2 )) * Y1);

          

           A18: x1 = ( [x1, y1] `1 ) & y1 = ( [x1, y1] `2 );

          x1 in INT & y1 in INT by INT_1:def 2;

          then

           A19: [x1, y1] in [: INT , INT :] by ZFMISC_1: 87;

          

           A20: ((x1 ^2 ) - (((a ^2 ) -' 1) * (y1 ^2 ))) = ((1 + (B * (Y1 ^2 ))) - (((a ^2 ) -' 1) * (y1 ^2 ))) by PELLS_EQ:def 1

          .= 1;

          then

           A21: [x1, y1] is Pell's_solution of ((a ^2 ) -' 1) by A18, A19, PELLS_EQ:def 1;

          ((2 * Y1) * y) >= (1 * 1) by A16, NAT_1: 14;

          then

           A22: (((2 * Y1) * y) * y) >= (1 * y) by XREAL_1: 66;

          

           A23: y1 > 0 by A22;

          then

           A24: (y1 ^2 ) >= 1 & y1 >= 1 by NAT_1: 14;

          y1 = ((y ^2 ) * (2 * Y1)) & y1 = ((2 * y) * (y * Y1));

          then

           A25: (y ^2 ) divides (y1 - 0 ) & (2 * y) divides y1 by INT_1:def 3;

          then

           A26: (y1, 0 ) are_congruent_mod (y ^2 ) by INT_1:def 4;

          (a ^2 ) >= (2 * a) & (a + a) > (a + 1) by A2, A1, NAT_2: 29, XREAL_1: 8, XREAL_1: 64;

          then (a ^2 ) > (a + 1) by XXREAL_0: 2;

          then

           A27: ((a ^2 ) -' 1) > a by A4, XREAL_1: 20;

          then

           A28: B > (a * 1) by A16, NAT_1: 14, XREAL_1: 97;

          (Y1 ^2 ) >= (1 ^2 ) by NAT_1: 14;

          then (1 + (B * (Y1 ^2 ))) > a by NAT_1: 13, A28, XREAL_1: 66;

          then ((x1 ^2 ) - a) >= (a - a) by A17, XREAL_1: 9;

          then

          reconsider x1a = ((x1 ^2 ) - a) as Element of NAT by INT_1: 3;

          set A = (a + ((x1 ^2 ) * x1a));

          A >= (2 + 0 ) by A3, XREAL_1: 7;

          then A <> 1 & A is non empty;

          then

          reconsider A as non trivial Nat by NAT_2: 28;

          (A - a) = (x1 * (x1 * x1a));

          then

           A29: (A,a) are_congruent_mod x1 by INT_1:def 4, INT_1:def 3;

          A = (a + ((1 + (((a ^2 ) -' 1) * (y1 ^2 ))) * ((1 + (((a ^2 ) -' 1) * (y1 ^2 ))) - a))) by A20;

          then

           A30: (A - 1) = (y1 * (y1 * ((((a ^2 ) -' 1) + ((1 + (((a ^2 ) -' 1) * (y1 ^2 ))) * ((a ^2 ) -' 1))) - (a * ((a ^2 ) -' 1)))));

          then

           A31: y1 divides (A - 1) by INT_1:def 3;

          then

           A32: (2 * y) divides (A - 1) by A25, INT_2: 9;

          

           A33: (A,1) are_congruent_mod (2 * y) by A31, A25, INT_2: 9, INT_1:def 4;

          (((a ^2 ) -' 1) * (y1 ^2 )) >= (a * 1) by A27, A24, XREAL_1: 66;

          then (2 + (((a ^2 ) -' 1) * (y1 ^2 ))) > ((a * 1) + 0 ) by XREAL_1: 8;

          then ((2 + (((a ^2 ) -' 1) * (y1 ^2 ))) - a) > (a - a) by XREAL_1: 9;

          then (y1 * (((a ^2 ) -' 1) * ((2 + (((a ^2 ) -' 1) * (y1 ^2 ))) - a))) >= (1 * 1) by A2, A23, NAT_1: 14;

          then (A - 1) >= (1 * y1) & (A - 0 ) > (A - 1) by A30, XREAL_1: 66, XREAL_1: 10;

          then A > y1 by XXREAL_0: 2;

          then

           A34: A > y by A22, XXREAL_0: 2;

          set x2 = ( Px (A,z)), y2 = ( Py (A,z));

          ((x2 ^2 ) - (((A ^2 ) -' 1) * (y2 ^2 ))) = 1 by Th10;

          then

           A35: [x2, y2] is Pell's_solution of ((A ^2 ) -' 1) by Lm3;

          (A - 1) divides (y2 - z) by Th27, INT_1:def 4;

          then (y2,z) are_congruent_mod (2 * y) by INT_1:def 4, A32, INT_2: 9;

          hence thesis by A5, A21, A6, A35, A2, A1, Th29, A29, A33, A26, A22, A34;

        end;

      end;

      given x,x1,y1,A,x2,y2 be Nat such that

       A36: a > 1 and

       A37: [x, y] is Pell's_solution of ((a ^2 ) -' 1) and

       A38: [x1, y1] is Pell's_solution of ((a ^2 ) -' 1) and

       A39: y1 >= y & A > y and

       A40: y >= z and

       A41: [x2, y2] is Pell's_solution of ((A ^2 ) -' 1) and

       A42: (y2,y) are_congruent_mod x1 and

       A43: (A,a) are_congruent_mod x1 and

       A44: (y2,z) are_congruent_mod (2 * y) and

       A45: (A,1) are_congruent_mod (2 * y) and

       A46: (y1, 0 ) are_congruent_mod (y ^2 );

      

       A47: a is non trivial by NAT_2: 28, A36;

      per cases ;

        suppose

         A48: y = 0 ;

        then z = 0 by A40;

        hence thesis by A36, A47, Th6, A48;

      end;

        suppose

         A49: y > 0 ;

        then y >= 1 by NAT_1: 14;

        then

        reconsider A as non trivial Nat by A39, NAT_2: 28;

        consider w be Nat such that

         A50: x = ( Px (a,w)) & y = ( Py (a,w)) by A47, A37, Th7;

        consider u be Nat such that

         A51: x1 = ( Px (a,u)) & y1 = ( Py (a,u)) by A47, A38, Th7;

        consider v be Nat such that

         A52: x2 = ( Px (A,v)) & y2 = ( Py (A,v)) by A41, Th7;

        

         A53: (y2,( Py (a,v))) are_congruent_mod x1 by A47, A43, A52, Th29;

        (y,y2) are_congruent_mod x1 by A42, INT_1: 14;

        then

         A54: (y,( Py (a,v))) are_congruent_mod ( Px (a,u)) by A51, A53, INT_1: 15;

        

         A55: u <> 0 by Th6, A51, A49, A39, A47;

        (( Py (A,v)),v) are_congruent_mod (2 * y)

        proof

          

           A56: (2 * y) divides (A - 1) by A45, INT_1:def 4;

          (A - 1) divides (( Py (A,v)) - v) by Th27, INT_1:def 4;

          hence thesis by INT_1:def 4, A56, INT_2: 9;

        end;

        then (v,y2) are_congruent_mod (2 * y) by A52, INT_1: 14;

        then

         A57: (v,z) are_congruent_mod (2 * y) by A44, INT_1: 15;

        

         A58: (y ^2 ) divides (y1 - 0 ) by A46, INT_1:def 4;

        

         A59: (z,v) are_congruent_mod (2 * y) by A57, INT_1: 14;

        

         A60: (( Py (a,v)),( Py (a,w))) are_congruent_mod ( Px (a,u)) by A54, A50, INT_1: 14;

        consider r be Integer such that

         A61: (y * r) = u by A58, A51, A50, Th40, INT_1:def 3, A47;

        

         A62: y >= w by A47, A50, Th16;

        

         A63: ( 0 - y) <= (z - w) <= (y - 0 ) by A40, A62, XREAL_1: 13;

        (y + 0 ) < (y + y) & (( - y) - y) < (( - y) - 0 ) by A49, XREAL_1: 6, XREAL_1: 15;

        then

         A64: (( - 1) * (2 * y)) < (z - w) < (1 * (2 * y)) by A63, XXREAL_0: 2;

        

         A65: ( 0 + 0 ) <= (z + w) <= (y + y) by A40, A62, XREAL_1: 7;

        per cases by A60, A55, Th36, A47;

          suppose (v,w) are_congruent_mod (2 * u);

          then

          consider t be Integer such that

           A66: (v - w) = ((2 * u) * t) by INT_1:def 5;

          (v - w) = ((2 * y) * (t * r)) by A66, A61;

          then (v,w) are_congruent_mod (2 * y) by INT_1:def 5;

          then

          consider i be Integer such that

           A67: (z - w) = ((2 * y) * i) by INT_1:def 5, A59, INT_1: 15;

          ( - 1) < i < ( 0 + 1) by A67, A64, XREAL_1: 64;

          then (( - 1) + 1) <= i & i <= 0 by INT_1: 7;

          then (z - w) = 0 by A67;

          hence y = ( Py (a,z)) & a > 1 by A36, A50;

        end;

          suppose (v,( - w)) are_congruent_mod (2 * u);

          then

          consider t be Integer such that

           A68: (v - ( - w)) = ((2 * u) * t) by INT_1:def 5;

          (v - ( - w)) = ((2 * y) * (t * r)) by A61, A68;

          then (v,( - w)) are_congruent_mod (2 * y) by INT_1:def 5;

          then

          consider i be Integer such that

           A69: (z - ( - w)) = ((2 * y) * i) by INT_1:def 5, A59, INT_1: 15;

          ((2 * y) * 0 ) <= ((2 * y) * i) <= ((2 * y) * 1) by A69, A65;

          then

           A70: 0 <= i <= 1 by A49, XREAL_1: 68;

          i < 1 or i = 1 by A70, XXREAL_0: 1;

          then

           A71: i = 0 or i = 1 by A70, NAT_1: 14;

          per cases by A71, A69;

            suppose (z + w) = 0 ;

            then z = 0 = w;

            hence thesis by A36, A50;

          end;

            suppose

             A72: (z + w) = (2 * y);

            

             A73: z = y

            proof

              assume z <> y;

              then z < y by A40, XXREAL_0: 1;

              then (z + w) < (y + y) by A47, A50, Th16, XREAL_1: 8;

              hence thesis by A72;

            end;

            w = y

            proof

              assume w <> y;

              then w < y by A62, XXREAL_0: 1;

              then (z + w) < (y + y) by A40, XREAL_1: 8;

              hence thesis by A72;

            end;

            hence thesis by A36, A73, A50;

          end;

        end;

      end;

    end;

    begin

    theorem :: HILB10_1:39

    for x,y,z be Nat holds y = (x |^ z) iff (y = 1 & z = 0 ) or (x = 0 & y = 0 & z > 0 ) or (x = 1 & y = 1 & z > 0 ) or (x > 1 & z > 0 & ex y1,y2,y3,K be Nat st y1 = ( Py (x,(z + 1))) & K > ((2 * z) * y1) & y2 = ( Py (K,(z + 1))) & y3 = ( Py ((K * x),(z + 1))) & ( 0 <= (y - (y3 / y2)) < (1 / 2) or 0 <= ((y3 / y2) - y) < (1 / 2)))

    proof

      let x,y,z be Nat;

      thus y = (x |^ z) implies (y = 1 & z = 0 ) or (x = 0 & y = 0 & z > 0 ) or (x = 1 & y = 1 & z > 0 ) or (x > 1 & z > 0 & ex y1,y2,y3,K be Nat st y1 = ( Py (x,(z + 1))) & K > ((2 * z) * y1) & y2 = ( Py (K,(z + 1))) & y3 = ( Py ((K * x),(z + 1))) & ( 0 <= (y - (y3 / y2)) < (1 / 2) or 0 <= ((y3 / y2) - y) < (1 / 2)))

      proof

        assume

         A1: y = (x |^ z);

        per cases ;

          suppose z = 0 ;

          hence thesis by A1, NEWTON: 4;

        end;

          suppose

           A2: z > 0 ;

          per cases by NAT_1: 53;

            suppose x = 0 or x = 1;

            hence thesis by A1, A2, NAT_1: 14, NEWTON: 11;

          end;

            suppose

             A3: x > 1;

            then

            reconsider x1 = x as non trivial Nat by NAT_2: 28;

            ex y1,y2,y3,K be Nat st y1 = ( Py (x1,(z + 1))) & K > ((2 * z) * y1) & y2 = ( Py (K,(z + 1))) & y3 = ( Py ((K * x1),(z + 1))) & ( 0 <= (y - (y3 / y2)) < (1 / 2) or 0 <= ((y3 / y2) - y) < (1 / 2))

            proof

              set y1 = ( Py (x1,(z + 1))), K = (((2 * z) * y1) + 1), y2 = ( Py (K,(z + 1))), y3 = ( Py ((K * x1),(z + 1)));

              reconsider K as non trivial Nat by A2;

              take y1, y2, y3, K;

              (x1 + (x1 - 1)) > (x1 + 0 ) by XREAL_1: 6;

              then

               A4: ((x1 + (x1 - 1)) to_power z) > (x1 to_power z) by A2, POWER: 37;

              (((2 * x1) - 1) |^ z) <= y1 by Th20;

              then y1 >= (x1 |^ z) by A4, XXREAL_0: 2;

              then K > ((2 * z) * (x1 |^ z)) by NAT_1: 13, XREAL_1: 64;

              then

               A5: (y - (1 / 2)) < (y3 / y2) < (y + (1 / 2)) by A1, Th22;

              (y - (y3 / y2)) >= 0 or ( - (y - (y3 / y2))) >= ( - 0 );

              hence thesis by NAT_1: 13, XREAL_1: 19, XREAL_1: 11, A5;

            end;

            hence thesis by A3, A2;

          end;

        end;

      end;

      assume

       A6: (y = 1 & z = 0 ) or (x = 0 & y = 0 & z > 0 ) or (x = 1 & y = 1 & z > 0 ) or (x > 1 & z > 0 & ex y1,y2,y3,K be Nat st y1 = ( Py (x,(z + 1))) & K > ((2 * z) * y1) & y2 = ( Py (K,(z + 1))) & y3 = ( Py ((K * x),(z + 1))) & ( 0 <= (y - (y3 / y2)) < (1 / 2) or 0 <= ((y3 / y2) - y) < (1 / 2)));

      per cases by A6;

        suppose y = 1 & z = 0 ;

        hence thesis by NEWTON: 4;

      end;

        suppose x = 0 & y = 0 & z > 0 ;

        hence thesis by NAT_1: 14, NEWTON: 11;

      end;

        suppose x = 1 & y = 1 & z > 0 ;

        hence thesis;

      end;

        suppose

         A7: x > 1 & z > 0 & ex y1,y2,y3,K be Nat st y1 = ( Py (x,(z + 1))) & K > ((2 * z) * y1) & y2 = ( Py (K,(z + 1))) & y3 = ( Py ((K * x),(z + 1))) & ( 0 <= (y - (y3 / y2)) < (1 / 2) or 0 <= ((y3 / y2) - y) < (1 / 2));

        reconsider x1 = x as non trivial Nat by A7, NAT_2: 28;

        consider y1,y2,y3,K be Nat such that

         A8: y1 = ( Py (x1,(z + 1))) and

         A9: K > ((2 * z) * y1) and

         A10: y2 = ( Py (K,(z + 1))) and

         A11: y3 = ( Py ((K * x1),(z + 1))) and

         A12: 0 <= (y - (y3 / y2)) < (1 / 2) or 0 <= ((y3 / y2) - y) < (1 / 2) by A7;

        ((2 * z) * y1) >= 1 by NAT_1: 14, A8, A7;

        then

        reconsider K as non trivial Nat by NAT_2: 28, A9;

        (x1 + (x1 - 1)) > (x1 + 0 ) by XREAL_1: 6;

        then

         A13: ((x1 + (x1 - 1)) to_power z) > (x1 to_power z) by A7, POWER: 37;

        (((2 * x1) - 1) |^ z) <= y1 by A8, Th20;

        then y1 >= (x1 |^ z) by A13, XXREAL_0: 2;

        then (y1 * (2 * z)) >= ((x1 |^ z) * (2 * z)) by XREAL_1: 64;

        then K > ((2 * z) * (x1 |^ z)) by A9, XXREAL_0: 2;

        then

         A14: ((x1 |^ z) - (1 / 2)) < (y3 / y2) < ((x1 |^ z) + (1 / 2)) by Th22, A10, A11;

        per cases by A12;

          suppose 0 <= (y - (y3 / y2)) < (1 / 2);

          then

           A15: (((x1 |^ z) - (1 / 2)) + 0 ) < ((y - (y3 / y2)) + (y3 / y2)) < ((1 / 2) + ((x1 |^ z) + (1 / 2))) by A14, XREAL_1: 8;

          then y < ((x1 |^ z) + 1);

          then

           A16: y <= (x1 |^ z) by INT_1: 7;

          ((x1 |^ z) - 1) < ((x1 |^ z) - (1 / 2)) by XREAL_1: 10;

          then ((x1 |^ z) - 1) < y by A15, XXREAL_0: 2;

          then (((x1 |^ z) - 1) + 1) <= y by INT_1: 7;

          hence thesis by A16, XXREAL_0: 1;

        end;

          suppose 0 <= ((y3 / y2) - y) < (1 / 2);

          then

           A17: (((x1 |^ z) - (1 / 2)) - (1 / 2)) < ((y3 / y2) - ((y3 / y2) - y)) < (((x1 |^ z) + (1 / 2)) - 0 ) by A14, XREAL_1: 14;

          then

           A18: (((x1 |^ z) - 1) + 1) <= y by INT_1: 7;

          ((x1 |^ z) + (1 / 2)) < ((x1 |^ z) + 1) by XREAL_1: 6;

          then y < ((x1 |^ z) + 1) by A17, XXREAL_0: 2;

          then y <= (x1 |^ z) by INT_1: 7;

          hence thesis by A18, XXREAL_0: 1;

        end;

      end;

    end;