hilb10_3.miz



    begin

    reserve n,m,k for Nat,

p,q for n -element XFinSequence of NAT ,

i1,i2,i3,i4,i5,i6 for Element of n,

a,b,c,d,e for Integer;

    registration

      let X be set, p be INT -valued Series of X, F_Real ;

      let a be integer Element of F_Real ;

      cluster (a * p) -> INT -valued;

      coherence

      proof

        thus ( rng (a * p)) c= INT

        proof

          let y be object such that

           A1: y in ( rng (a * p));

          consider x be object such that

           A2: x in ( dom (a * p)) & ((a * p) . x) = y by A1, FUNCT_1:def 3;

          reconsider x as bag of X by A2;

          ((a * p) . x) = (a * (p . x)) by POLYNOM7:def 9;

          hence thesis by A2, INT_1:def 2;

        end;

      end;

    end

    theorem :: HILB10_3:1

    

     Th1: for O be non empty Ordinal, i be Element of O, L be add-associative right_zeroed right_complementable well-unital distributive non trivial doubleLoopStr holds for x be Function of O, L holds ( eval (( 1_1 (i,L)),x)) = (x . i)

    proof

      let O be non empty Ordinal, i be Element of O, L be add-associative right_zeroed right_complementable well-unital distributive non trivial doubleLoopStr;

      let x be Function of O, L;

      set p = ( 1_1 (i,L));

      ( Support p) = {( UnitBag i)} by HILBASIS: 13;

      

      then ( eval (p,x)) = ((p . ( UnitBag i)) * ( eval (( UnitBag i),x))) by POLYNOM2: 19

      .= (( 1_ L) * ( eval (( UnitBag i),x))) by HILBASIS: 12

      .= ( eval (( UnitBag i),x));

      hence thesis by HILBASIS: 11;

    end;

    theorem :: HILB10_3:2

    

     Th2: i1 is Element of (n + k)

    proof

      i1 is Element of ( Segm n);

      then

      reconsider I = i1 as Nat;

      per cases ;

        suppose n = 0 & k = 0 ;

        hence thesis;

      end;

        suppose

         A1: n = 0 & k > 0 ;

        then i1 is empty by SUBSET_1:def 1;

        then I in ( Segm (n + k)) by A1, NAT_1: 44;

        hence thesis;

      end;

        suppose n <> 0 ;

        then I in ( Segm n);

        then I < n <= (n + k) by NAT_1: 11, NAT_1: 44;

        then I < (n + k) by XXREAL_0: 2;

        then I in ( Segm (n + k)) by NAT_1: 44;

        hence thesis;

      end;

    end;

    theorem :: HILB10_3:3

    

     Th3: k < m implies (n + k) in (n + m)

    proof

      assume m > k;

      then (k + n) < (n + m) by XREAL_1: 8;

      then (n + k) in ( Segm (n + m)) by NAT_1: 44;

      hence thesis;

    end;

    theorem :: HILB10_3:4

    

     Th4: for p be (n + k) -element XFinSequence st n <> 0 & k <> 0 holds ((p | n) . i1) = (p . i1)

    proof

      let p be (n + k) -element XFinSequence such that

       A1: n <> 0 and

       A2: k <> 0 ;

      i1 is Element of ( Segm n);

      then

      reconsider I = i1 as Nat;

      k > 0 by A2;

      then

       A3: ( len p) = (n + k) & (n + k) > (n + 0 ) by CARD_1:def 7, XREAL_1: 8;

      I in n by A1;

      hence thesis by A3, AFINSQ_1: 53;

    end;

    begin

    theorem :: HILB10_3:5

    

     Th5: for A be diophantine Subset of (n -xtuples_of NAT ) holds for k st k <= n holds { (p | k) : p in A } is diophantine Subset of (k -xtuples_of NAT )

    proof

      let A be diophantine Subset of (n -xtuples_of NAT );

      let k such that

       A1: k <= n;

      consider nA be Nat, pA be INT -valued Polynomial of (n + nA), F_Real such that

       A2: for s be object holds s in A iff ex x be n -element XFinSequence of NAT , y be nA -element XFinSequence of NAT st s = x & ( eval (pA,( @ (x ^ y)))) = 0 by HILB10_2:def 6;

      set D = { (p | k) where p be n -element XFinSequence of NAT : p in A };

      D c= (k -xtuples_of NAT )

      proof

        let y be object;

        assume y in D;

        then

        consider p be n -element XFinSequence of NAT such that

         A3: y = (p | k) & p in A;

        ( len p) = n by CARD_1:def 7;

        then ( len (p | k)) = k by A1, AFINSQ_1: 54;

        then (p | k) is k -element by CARD_1:def 7;

        hence thesis by A3, HILB10_2:def 5;

      end;

      then

      reconsider D as Subset of (k -xtuples_of NAT );

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

      reconsider P = pA as INT -valued Polynomial of (k + (nk + nA)), F_Real ;

      for s be object holds s in D iff ex x be k -element XFinSequence of NAT , y be (nk + nA) -element XFinSequence of NAT st s = x & ( eval (P,( @ (x ^ y)))) = 0

      proof

        let s be object;

        thus s in D implies ex x be k -element XFinSequence of NAT , y be (nk + nA) -element XFinSequence of NAT st s = x & ( eval (P,( @ (x ^ y)))) = 0

        proof

          assume s in D;

          then

          consider p be n -element XFinSequence of NAT such that

           A4: s = (p | k) & p in A;

          consider x be n -element XFinSequence of NAT , y be nA -element XFinSequence of NAT such that

           A5: p = x & ( eval (pA,( @ (x ^ y)))) = 0 by A4, A2;

          

           A6: x = ((x | k) ^ (x /^ k));

          

           A7: ( len x) = n & ( len y) = nA by CARD_1:def 7;

          then

           A8: ( len (x | k)) = k by A1, AFINSQ_1: 54;

          ( len (x /^ k)) = ((k + nk) -' k) by A7, AFINSQ_2:def 2

          .= nk by NAT_D: 34;

          then ( len ((x /^ k) ^ y)) = (nk + nA) by A7, AFINSQ_1: 17;

          then

          reconsider X = ((x /^ k) ^ y) as (nk + nA) -element XFinSequence of NAT by CARD_1:def 7;

          

           A9: (x ^ y) = ((x | k) ^ X) by A6, AFINSQ_1: 27;

          reconsider xk = (x | k) as k -element XFinSequence of NAT by A8, CARD_1:def 7;

          s = xk by A4, A5;

          hence thesis by A9, A5;

        end;

        given x be k -element XFinSequence of NAT , y be (nk + nA) -element XFinSequence of NAT such that

         A10: s = x & ( eval (P,( @ (x ^ y)))) = 0 ;

        

         A11: y = ((y | nk) ^ (y /^ nk));

        

         A12: ( len x) = k & ( len y) = (nk + nA) by CARD_1:def 7;

        then

         A13: ( len (y | nk)) = nk by NAT_1: 11, AFINSQ_1: 54;

        

         A14: ( len (y /^ nk)) = ((nk + nA) -' nk) by A12, AFINSQ_2:def 2

        .= nA by NAT_D: 34;

        ( len (x ^ (y | nk))) = (k + nk) by A12, A13, AFINSQ_1: 17;

        then

        reconsider X = (x ^ (y | nk)) as n -element XFinSequence of NAT by CARD_1:def 7;

        reconsider Y = (y /^ nk) as nA -element XFinSequence of NAT by CARD_1:def 7, A14;

        (x ^ y) = (X ^ Y) by A11, AFINSQ_1: 27;

        then X in A by A2, A10;

        then (X | k) in D;

        hence thesis by A10, A12, AFINSQ_1: 57;

      end;

      hence thesis by HILB10_2:def 6;

    end;

    theorem :: HILB10_3:6

    

     Th6: for a,b,c be Integer, i1, i2 holds { p : (a * (p . i1)) = ((b * (p . i2)) + c) } is diophantine Subset of (n -xtuples_of NAT )

    proof

      let c,a,b be Integer, i1, i2;

      set F = F_Real ;

      reconsider ar = a, br = b, cr = c as integer Element of F by XREAL_0:def 1;

      set D = { p : (c * (p . i1)) = ((a * (p . i2)) + b) };

      D c= (n -xtuples_of NAT )

      proof

        let y be object;

        assume y in D;

        then ex p st y = p & (c * (p . i1)) = ((a * (p . i2)) + b);

        hence thesis by HILB10_2:def 5;

      end;

      then

      reconsider D as Subset of (n -xtuples_of NAT );

      per cases ;

        suppose n = 0 ;

        then D is diophantine Subset of (n -xtuples_of NAT );

        hence thesis;

      end;

        suppose

         A1: n <> 0 ;

        set Q = (((cr * ( 1_1 (i1,F))) - (ar * ( 1_1 (i2,F)))) - (br * ( 1_ (n,F))));

        reconsider Q as INT -valued Polynomial of (n + 0 ), F_Real ;

        for s be object holds s in D iff ex x be n -element XFinSequence of NAT , y be 0 -element XFinSequence of NAT st s = x & ( eval (Q,( @ (x ^ y)))) = 0

        proof

          let s be object;

          thus s in D implies ex x be n -element XFinSequence of NAT , y be 0 -element XFinSequence of NAT st s = x & ( eval (Q,( @ (x ^ y)))) = 0

          proof

            assume s in D;

            then

            consider p such that

             A2: s = p & (c * (p . i1)) = ((a * (p . i2)) + b);

            reconsider Z = ( <%> NAT ) as 0 -element XFinSequence of NAT ;

            take pZ = p, Z;

            

             A3: ( eval ((br * ( 1_ (n,F))),( @ p))) = (br * ( eval (( 1_ (n,F)),( @ p)))) by POLYNOM7: 29

            .= (br * ( 1. F)) by POLYNOM2: 21

            .= b;

            

             A4: ( eval ((ar * ( 1_1 (i2,F))),( @ p))) = (ar * ( eval (( 1_1 (i2,F)),( @ p)))) by POLYNOM7: 29

            .= (a * (p . i2)) by A1, Th1;

            

             A5: ( eval ((cr * ( 1_1 (i1,F))),( @ p))) = (cr * ( eval (( 1_1 (i1,F)),( @ p)))) by POLYNOM7: 29

            .= (c * (p . i1)) by A1, Th1;

            ( eval (Q,( @ (p ^ Z)))) = (( eval (((cr * ( 1_1 (i1,F))) - (ar * ( 1_1 (i2,F)))),( @ p))) - ( eval ((br * ( 1_ (n,F))),( @ p)))) by POLYNOM2: 24

            .= ((( eval ((cr * ( 1_1 (i1,F))),( @ p))) - ( eval ((ar * ( 1_1 (i2,F))),( @ p)))) - ( eval ((br * ( 1_ (n,F))),( @ p)))) by POLYNOM2: 24

            .= 0 by A2, A3, A4, A5;

            hence thesis by A2;

          end;

          given p be n -element XFinSequence of NAT , Z be 0 -element XFinSequence of NAT such that

           A6: s = p & ( eval (Q,( @ (p ^ Z)))) = 0 ;

          

           A7: ( eval ((br * ( 1_ (n,F))),( @ p))) = (br * ( eval (( 1_ (n,F)),( @ p)))) by POLYNOM7: 29

          .= (br * ( 1. F)) by POLYNOM2: 21

          .= b;

          

           A8: ( eval ((ar * ( 1_1 (i2,F))),( @ p))) = (ar * ( eval (( 1_1 (i2,F)),( @ p)))) by POLYNOM7: 29

          .= (a * (p . i2)) by A1, Th1;

          

           A9: ( eval ((cr * ( 1_1 (i1,F))),( @ p))) = (cr * ( eval (( 1_1 (i1,F)),( @ p)))) by POLYNOM7: 29

          .= (c * (p . i1)) by A1, Th1;

          ( eval (Q,( @ (p ^ Z)))) = (( eval (((cr * ( 1_1 (i1,F))) - (ar * ( 1_1 (i2,F)))),( @ p))) - ( eval ((br * ( 1_ (n,F))),( @ p)))) by POLYNOM2: 24

          .= ((( eval ((cr * ( 1_1 (i1,F))),( @ p))) - ( eval ((ar * ( 1_1 (i2,F))),( @ p)))) - ( eval ((br * ( 1_ (n,F))),( @ p)))) by POLYNOM2: 24

          .= (((c * (p . i1)) - (a * (p . i2))) - b) by A7, A8, A9;

          then (c * (p . i1)) = ((a * (p . i2)) + b) by A6;

          hence thesis by A6;

        end;

        then D is diophantine;

        hence thesis;

      end;

    end;

    theorem :: HILB10_3:7

    

     Th7: for a, b, c, i1, i2 holds { p : (a * (p . i1)) > ((b * (p . i2)) + c) } is diophantine Subset of (n -xtuples_of NAT )

    proof

      let a,b,c be Integer, i1,i2 be Element of n;

      set F = F_Real ;

      set n1 = (n + 1);

      set D = { p : (a * (p . i1)) > ((b * (p . i2)) + c) };

      D c= (n -xtuples_of NAT )

      proof

        let y be object;

        assume y in D;

        then ex p st y = p & (a * (p . i1)) > ((b * (p . i2)) + c);

        hence thesis by HILB10_2:def 5;

      end;

      then

      reconsider D as Subset of (n -xtuples_of NAT );

      per cases ;

        suppose n = 0 ;

        then D is diophantine Subset of (n -xtuples_of NAT );

        hence thesis;

      end;

        suppose

         A1: n <> 0 ;

        

         A2: n < n1 by NAT_1: 13;

        n in ( Segm n1) by A2, NAT_1: 44;

        then

        reconsider I = i1, J = i2, N = n as Element of n1 by Th2;

        reconsider ar = a, br = b, cr = (c + 1) as integer Element of F by XREAL_0:def 1;

        set Q = ((((br * ( 1_1 (J,F))) - (ar * ( 1_1 (I,F)))) + ( 1_1 (N,F))) + (cr * ( 1_ (n1,F))));

        reconsider Q as INT -valued Polynomial of (n + 1), F_Real ;

        for s be object holds s in D iff ex x be n -element XFinSequence of NAT , y be 1 -element XFinSequence of NAT st s = x & ( eval (Q,( @ (x ^ y)))) = 0

        proof

          let s be object;

          thus s in D implies ex x be n -element XFinSequence of NAT , y be 1 -element XFinSequence of NAT st s = x & ( eval (Q,( @ (x ^ y)))) = 0

          proof

            assume s in D;

            then

            consider p such that

             A3: s = p & (a * (p . i1)) > ((b * (p . i2)) + c);

            ((a * (p . i1)) - ((b * (p . i2)) + c)) > 0 by A3, XREAL_1: 50;

            then

            reconsider pij = ((a * (p . i1)) - ((b * (p . i2)) + c)) as Element of NAT by INT_1: 3;

            reconsider pp = (pij - 1) as Element of NAT by A3, XREAL_1: 50, NAT_1: 20;

            reconsider Z = <%pp%> as 1 -element XFinSequence of NAT ;

            take pZ = p, Z;

            set P = ( @ (p ^ Z));

            

             A4: ( len p) = n by CARD_1:def 7;

            

             A5: (P . I) = (p . i1) & (P . J) = (p . i2) by A4, A1, AFINSQ_1:def 3;

            

             A6: ( eval ((ar * ( 1_1 (I,F))),P)) = (ar * ( eval (( 1_1 (I,F)),P))) by POLYNOM7: 29

            .= (a * (P . I)) by Th1;

            

             A7: ( eval ((br * ( 1_1 (J,F))),P)) = (br * ( eval (( 1_1 (J,F)),P))) by POLYNOM7: 29

            .= (b * (P . J)) by Th1;

            

             A8: ( eval ((cr * ( 1_ (n1,F))),P)) = (cr * ( eval (( 1_ (n1,F)),P))) by POLYNOM7: 29

            .= (cr * ( 1. F)) by POLYNOM2: 21;

            

             A9: ( eval (( 1_1 (I,F)),P)) = (P . I) & ( eval (( 1_1 (J,F)),P)) = (P . J) & ( eval (( 1_1 (N,F)),P)) = (P . N) & ( eval (( 1_ (n1,F)),P)) = ( 1. F) by Th1, POLYNOM2: 21;

            ( eval (Q,P)) = (( eval ((((br * ( 1_1 (J,F))) - (ar * ( 1_1 (I,F)))) + ( 1_1 (N,F))),P)) + ( eval ((cr * ( 1_ (n1,F))),P))) by POLYNOM2: 23

            .= ((( eval (((br * ( 1_1 (J,F))) - (ar * ( 1_1 (I,F)))),P)) + ( eval (( 1_1 (N,F)),P))) + ( eval ((cr * ( 1_ (n1,F))),P))) by POLYNOM2: 23

            .= (((( eval ((br * ( 1_1 (J,F))),P)) - ( eval ((ar * ( 1_1 (I,F))),P))) + ( eval (( 1_1 (N,F)),P))) + ( eval ((cr * ( 1_ (n1,F))),P))) by POLYNOM2: 24

            .= ((((b * (p . i2)) - (a * (p . i1))) + pp) + cr) by A4, AFINSQ_1: 36, A5, A9, A6, A7, A8

            .= 0 ;

            hence thesis by A3;

          end;

          given p be n -element XFinSequence of NAT , Z be 1 -element XFinSequence of NAT such that

           A10: s = p & ( eval (Q,( @ (p ^ Z)))) = 0 ;

          set P = ( @ (p ^ Z));

          ( len p) = n by CARD_1:def 7;

          then

           A11: (P . I) = (p . i1) & (P . J) = (p . i2) by A1, AFINSQ_1:def 3;

          

           A12: ( eval ((ar * ( 1_1 (I,F))),P)) = (ar * ( eval (( 1_1 (I,F)),P))) by POLYNOM7: 29

          .= (a * (P . I)) by Th1;

          

           A13: ( eval ((br * ( 1_1 (J,F))),P)) = (br * ( eval (( 1_1 (J,F)),P))) by POLYNOM7: 29

          .= (b * (P . J)) by Th1;

          

           A14: ( eval ((cr * ( 1_ (n1,F))),P)) = (cr * ( eval (( 1_ (n1,F)),P))) by POLYNOM7: 29

          .= (cr * ( 1. F)) by POLYNOM2: 21;

          ( eval (Q,P)) = (( eval ((((br * ( 1_1 (J,F))) - (ar * ( 1_1 (I,F)))) + ( 1_1 (N,F))),P)) + ( eval ((cr * ( 1_ (n1,F))),P))) by POLYNOM2: 23

          .= ((( eval (((br * ( 1_1 (J,F))) - (ar * ( 1_1 (I,F)))),P)) + ( eval (( 1_1 (N,F)),P))) + ( eval ((cr * ( 1_ (n1,F))),P))) by POLYNOM2: 23

          .= (((( eval ((br * ( 1_1 (J,F))),P)) - ( eval ((ar * ( 1_1 (I,F))),P))) + ( eval (( 1_1 (N,F)),P))) + ( eval ((cr * ( 1_ (n1,F))),P))) by POLYNOM2: 24

          .= ((((b * (p . i2)) - (a * (p . i1))) + (P . n)) + cr) by Th1, A11, A12, A13, A14;

          then (a * (p . i1)) = ((((b * (p . i2)) + c) + 1) + (P . n)) by A10;

          then

           A15: (a * (p . i1)) >= (((b * (p . i2)) + c) + 1) by XREAL_1: 31;

          (((b * (p . i2)) + c) + 1) > ((b * (p . i2)) + c) by XREAL_1: 29;

          then (a * (p . i1)) > ((b * (p . i2)) + c) by A15, XXREAL_0: 2;

          hence thesis by A10;

        end;

        then D is diophantine;

        hence thesis;

      end;

    end;

    scheme :: HILB10_3:sch1

    UnionDiophantine { n() -> Nat , P,Q[ XFinSequence of NAT ] } :

{ p where p be n() -element XFinSequence of NAT : P[p] or Q[p] } is diophantine Subset of (n() -xtuples_of NAT )

      provided

       A1: { p where p be n() -element XFinSequence of NAT : P[p] } is diophantine Subset of (n() -xtuples_of NAT )

       and

       A2: { p where p be n() -element XFinSequence of NAT : Q[p] } is diophantine Subset of (n() -xtuples_of NAT );

      reconsider PF = { p where p be n() -element XFinSequence of NAT : P[p] } as diophantine Subset of (n() -xtuples_of NAT ) by A1;

      reconsider QF = { p where p be n() -element XFinSequence of NAT : Q[p] } as diophantine Subset of (n() -xtuples_of NAT ) by A2;

      set PQ = { p where p be n() -element XFinSequence of NAT : P[p] or Q[p] };

      

       A3: PQ c= (PF \/ QF)

      proof

        let x be object;

        assume x in PQ;

        then

        consider p be n() -element XFinSequence of NAT such that

         A4: x = p & (P[p] or Q[p]);

        x in PF or x in QF by A4;

        hence thesis by XBOOLE_0:def 3;

      end;

      

       A5: PF c= PQ

      proof

        let x be object;

        assume x in PF;

        then ex p be n() -element XFinSequence of NAT st x = p & P[p];

        hence thesis;

      end;

      QF c= PQ

      proof

        let x be object;

        assume x in QF;

        then ex p be n() -element XFinSequence of NAT st x = p & Q[p];

        hence thesis;

      end;

      then (PF \/ QF) c= PQ by A5, XBOOLE_1: 8;

      hence thesis by A3, XBOOLE_0:def 10;

    end;

    scheme :: HILB10_3:sch2

    Eq { n() -> Nat , P,Q[ object] } :

{ p where p be n() -element XFinSequence of NAT : P[p] } = { q where q be n() -element XFinSequence of NAT : Q[q] }

      provided

       A1: for p be n() -element XFinSequence of NAT holds P[p] iff Q[p];

      set P = { p where p be n() -element XFinSequence of NAT : P[p] }, Q = { q where q be n() -element XFinSequence of NAT : Q[q] };

      thus P c= Q

      proof

        let x be object such that

         A2: x in P;

        consider p be n() -element XFinSequence of NAT such that

         A3: x = p & P[p] by A2;

        Q[p] by A1, A3;

        hence thesis by A3;

      end;

      let x be object such that

       A4: x in Q;

      consider p be n() -element XFinSequence of NAT such that

       A5: x = p & Q[p] by A4;

      P[p] by A1, A5;

      hence thesis by A5;

    end;

    theorem :: HILB10_3:8

    

     Th8: for a, b, c, i1, i2 holds { p : (a * (p . i1)) >= ((b * (p . i2)) + c) } is diophantine Subset of (n -xtuples_of NAT )

    proof

      let a,b,c be Integer, i1,i2 be Element of n;

      defpred P[ XFinSequence of NAT ] means (a * ($1 . i1)) > ((b * ($1 . i2)) + c);

      defpred Q[ XFinSequence of NAT ] means (a * ($1 . i1)) = ((b * ($1 . i2)) + c);

      defpred R[ XFinSequence of NAT ] means P[$1] or Q[$1];

      defpred S[ XFinSequence of NAT ] means (a * ($1 . i1)) >= ((b * ($1 . i2)) + c);

      

       A1: { p : P[p] } is diophantine Subset of (n -xtuples_of NAT ) by Th7;

      

       A2: { p : Q[p] } is diophantine Subset of (n -xtuples_of NAT ) by Th6;

      

       A3: { p : P[p] or Q[p] } is diophantine Subset of (n -xtuples_of NAT ) from UnionDiophantine( A1, A2);

      

       A4: R[p] iff S[p] by XXREAL_0: 1;

      { p : R[p] } = { q : S[q] } from Eq( A4);

      hence thesis by A3;

    end;

    theorem :: HILB10_3:9

    

     Th9: for a, b, i1, i2, i3 holds { p : (a * (p . i1)) = ((b * (p . i2)) * (p . i3)) } is diophantine Subset of (n -xtuples_of NAT )

    proof

      let a,b be Integer, i1, i2, i3;

      set F = F_Real ;

      reconsider ar = a, br = b as integer Element of F by XREAL_0:def 1;

      set D = { p : (a * (p . i1)) = ((b * (p . i2)) * (p . i3)) };

      D c= (n -xtuples_of NAT )

      proof

        let y be object;

        assume y in D;

        then ex p st y = p & (a * (p . i1)) = ((b * (p . i2)) * (p . i3));

        hence thesis by HILB10_2:def 5;

      end;

      then

      reconsider D as Subset of (n -xtuples_of NAT );

      per cases ;

        suppose n = 0 ;

        then D is diophantine Subset of (n -xtuples_of NAT );

        hence thesis;

      end;

        suppose

         A1: n <> 0 ;

        set Q = ((ar * ( 1_1 (i1,F))) - (br * (( 1_1 (i2,F)) *' ( 1_1 (i3,F)))));

        reconsider Q as INT -valued Polynomial of (n + 0 ), F_Real ;

        for s be object holds s in D iff ex x be n -element XFinSequence of NAT , y be 0 -element XFinSequence of NAT st s = x & ( eval (Q,( @ (x ^ y)))) = 0

        proof

          let s be object;

          thus s in D implies ex x be n -element XFinSequence of NAT , y be 0 -element XFinSequence of NAT st s = x & ( eval (Q,( @ (x ^ y)))) = 0

          proof

            assume s in D;

            then

            consider p such that

             A2: s = p & (a * (p . i1)) = ((b * (p . i2)) * (p . i3));

            reconsider Z = ( <%> NAT ) as 0 -element XFinSequence of NAT ;

            take p, Z;

            set pZ = (p ^ Z);

            

             A3: ( eval (( 1_1 (i1,F)),( @ p))) = (p . i1) & ( eval (( 1_1 (i2,F)),( @ p))) = (p . i2) & ( eval (( 1_1 (i3,F)),( @ p))) = (p . i3) by A1, Th1;

            

             A4: ( eval ((ar * ( 1_1 (i1,F))),( @ p))) = (ar * ( eval (( 1_1 (i1,F)),( @ p)))) by POLYNOM7: 29

            .= (a * (p . i1)) by A1, Th1;

            

             A5: ( eval ((br * (( 1_1 (i2,F)) *' ( 1_1 (i3,F)))),( @ p))) = (br * ( eval ((( 1_1 (i2,F)) *' ( 1_1 (i3,F))),( @ p)))) by POLYNOM7: 29

            .= (br * (( eval (( 1_1 (i2,F)),( @ p))) * ( eval (( 1_1 (i3,F)),( @ p))))) by POLYNOM2: 25

            .= (b * ((p . i2) * (p . i3))) by A3;

            ( eval (Q,( @ pZ))) = (( eval ((ar * ( 1_1 (i1,F))),( @ p))) - ( eval ((br * (( 1_1 (i2,F)) *' ( 1_1 (i3,F)))),( @ p)))) by POLYNOM2: 24

            .= 0 by A2, A4, A5;

            hence thesis by A2;

          end;

          given p be n -element XFinSequence of NAT , Z be 0 -element XFinSequence of NAT such that

           A6: s = p & ( eval (Q,( @ (p ^ Z)))) = 0 ;

          

           A7: ( eval (( 1_1 (i1,F)),( @ p))) = (p . i1) & ( eval (( 1_1 (i2,F)),( @ p))) = (p . i2) & ( eval (( 1_1 (i3,F)),( @ p))) = (p . i3) by A1, Th1;

          

           A8: ( eval ((br * (( 1_1 (i2,F)) *' ( 1_1 (i3,F)))),( @ p))) = (br * ( eval ((( 1_1 (i2,F)) *' ( 1_1 (i3,F))),( @ p)))) by POLYNOM7: 29

          .= (br * (( eval (( 1_1 (i2,F)),( @ p))) * ( eval (( 1_1 (i3,F)),( @ p))))) by POLYNOM2: 25

          .= (b * ((p . i2) * (p . i3))) by A7;

          

           A9: ( eval ((ar * ( 1_1 (i1,F))),( @ p))) = (ar * ( eval (( 1_1 (i1,F)),( @ p)))) by POLYNOM7: 29

          .= (a * (p . i1)) by A1, Th1;

          set P = (p ^ Z);

          ( eval (Q,( @ P))) = (( eval ((ar * ( 1_1 (i1,F))),( @ p))) - ( eval ((br * (( 1_1 (i2,F)) *' ( 1_1 (i3,F)))),( @ p)))) by POLYNOM2: 24

          .= ((a * (p . i1)) - (b * ((p . i2) * (p . i3)))) by A8, A9;

          then (a * (p . i1)) = ((b * (p . i2)) * (p . i3)) by A6;

          hence s in D by A6;

        end;

        then D is diophantine;

        hence thesis;

      end;

    end;

    theorem :: HILB10_3:10

    

     Th10: for a, b, c, i1, i2, i3 holds { p : ex z be Nat st (a * (p . i1)) = ((b * (p . i2)) + ((z * c) * (p . i3))) } is diophantine Subset of (n -xtuples_of NAT )

    proof

      let a,b,c be Integer, i1,i2,i3 be Element of n;

      set F = F_Real ;

      set n1 = (n + 1);

      set D = { p : ex z be Nat st (a * (p . i1)) = ((b * (p . i2)) + ((z * c) * (p . i3))) };

      D c= (n -xtuples_of NAT )

      proof

        let y be object;

        assume y in D;

        then ex p st y = p & ex z be Nat st (a * (p . i1)) = ((b * (p . i2)) + ((z * c) * (p . i3)));

        hence thesis by HILB10_2:def 5;

      end;

      then

      reconsider D as Subset of (n -xtuples_of NAT );

      per cases ;

        suppose n = 0 ;

        then D is diophantine Subset of (n -xtuples_of NAT );

        hence thesis;

      end;

        suppose

         A1: n <> 0 ;

        

         A2: n < n1 by NAT_1: 13;

        n in ( Segm n1) by A2, NAT_1: 44;

        then

        reconsider I = i1, J = i2, K = i3, N = n as Element of n1 by Th2;

        reconsider ar = a, br = b, cr = c as integer Element of F by XREAL_0:def 1;

        set Q = (((ar * ( 1_1 (I,F))) - (br * ( 1_1 (J,F)))) - (cr * (( 1_1 (K,F)) *' ( 1_1 (N,F)))));

        reconsider Q as INT -valued Polynomial of (n + 1), F_Real ;

        for s be object holds s in D iff ex x be n -element XFinSequence of NAT , y be 1 -element XFinSequence of NAT st s = x & ( eval (Q,( @ (x ^ y)))) = 0

        proof

          let s be object;

          thus s in D implies ex x be n -element XFinSequence of NAT , y be 1 -element XFinSequence of NAT st s = x & ( eval (Q,( @ (x ^ y)))) = 0

          proof

            assume s in D;

            then

            consider p such that

             A3: s = p & ex z be Nat st (a * (p . i1)) = ((b * (p . i2)) + ((z * c) * (p . i3)));

            consider z be Nat such that

             A4: (a * (p . i1)) = ((b * (p . i2)) + ((z * c) * (p . i3))) by A3;

            reconsider z as Element of NAT by ORDINAL1:def 12;

            reconsider Z = <%z%> as 1 -element XFinSequence of NAT ;

            take p, Z;

            set P = ( @ (p ^ Z));

            

             A5: ( len p) = n by CARD_1:def 7;

            then

             A6: (P . I) = (p . i1) & (P . J) = (p . i2) & (P . K) = (p . i3) by A1, AFINSQ_1:def 3;

            

             A7: ( eval (( 1_1 (I,F)),P)) = (P . I) & ( eval (( 1_1 (J,F)),P)) = (P . J) & ( eval (( 1_1 (K,F)),P)) = (P . K) & ( eval (( 1_1 (N,F)),P)) = (P . N) & ( eval (( 1_ (n1,F)),P)) = ( 1. F) by Th1, POLYNOM2: 21;

            

             A8: ( eval ((cr * (( 1_1 (K,F)) *' ( 1_1 (N,F)))),P)) = (cr * ( eval ((( 1_1 (K,F)) *' ( 1_1 (N,F))),P))) by POLYNOM7: 29

            .= (cr * (( eval (( 1_1 (K,F)),P)) * ( eval (( 1_1 (N,F)),P)))) by POLYNOM2: 25

            .= (c * ((P . K) * (P . N))) by A7;

            ( eval (Q,P)) = (( eval (((ar * ( 1_1 (I,F))) - (br * ( 1_1 (J,F)))),P)) - ( eval ((cr * (( 1_1 (K,F)) *' ( 1_1 (N,F)))),P))) by POLYNOM2: 24

            .= ((( eval ((ar * ( 1_1 (I,F))),P)) - ( eval ((br * ( 1_1 (J,F))),P))) - ( eval ((cr * (( 1_1 (K,F)) *' ( 1_1 (N,F)))),P))) by POLYNOM2: 24

            .= (((ar * ( eval (( 1_1 (I,F)),P))) - ( eval ((br * ( 1_1 (J,F))),P))) - ( eval ((cr * (( 1_1 (K,F)) *' ( 1_1 (N,F)))),P))) by POLYNOM7: 29

            .= (((ar * ( eval (( 1_1 (I,F)),P))) - (br * ( eval (( 1_1 (J,F)),P)))) - ( eval ((cr * (( 1_1 (K,F)) *' ( 1_1 (N,F)))),P))) by POLYNOM7: 29

            .= (((ar * (P . I)) - (br * (P . J))) - ((c * (P . K)) * (P . N))) by A7, A8

            .= (((a * (p . i1)) - (b * (p . i2))) - ((c * (p . i3)) * z)) by A5, AFINSQ_1: 36, A6

            .= 0 by A4;

            hence thesis by A3;

          end;

          given p be n -element XFinSequence of NAT , Z be 1 -element XFinSequence of NAT such that

           A9: s = p & ( eval (Q,( @ (p ^ Z)))) = 0 ;

          set P = ( @ (p ^ Z));

          ( len p) = n by CARD_1:def 7;

          then

           A10: (P . I) = (p . i1) & (P . J) = (p . i2) & (P . K) = (p . i3) by A1, AFINSQ_1:def 3;

          

           A11: ( eval (( 1_1 (I,F)),P)) = (P . I) & ( eval (( 1_1 (J,F)),P)) = (P . J) & ( eval (( 1_1 (K,F)),P)) = (P . K) & ( eval (( 1_1 (N,F)),P)) = (P . N) & ( eval (( 1_ (n1,F)),P)) = ( 1. F) by Th1, POLYNOM2: 21;

          

           A12: ( eval ((cr * (( 1_1 (K,F)) *' ( 1_1 (N,F)))),P)) = (cr * ( eval ((( 1_1 (K,F)) *' ( 1_1 (N,F))),P))) by POLYNOM7: 29

          .= (cr * (( eval (( 1_1 (K,F)),P)) * ( eval (( 1_1 (N,F)),P)))) by POLYNOM2: 25

          .= (c * ((P . K) * (P . N))) by A11;

          ( eval (Q,P)) = (( eval (((ar * ( 1_1 (I,F))) - (br * ( 1_1 (J,F)))),P)) - ( eval ((cr * (( 1_1 (K,F)) *' ( 1_1 (N,F)))),P))) by POLYNOM2: 24

          .= ((( eval ((ar * ( 1_1 (I,F))),P)) - ( eval ((br * ( 1_1 (J,F))),P))) - ( eval ((cr * (( 1_1 (K,F)) *' ( 1_1 (N,F)))),P))) by POLYNOM2: 24

          .= (((ar * ( eval (( 1_1 (I,F)),P))) - ( eval ((br * ( 1_1 (J,F))),P))) - ( eval ((cr * (( 1_1 (K,F)) *' ( 1_1 (N,F)))),P))) by POLYNOM7: 29

          .= (((ar * ( eval (( 1_1 (I,F)),P))) - (br * ( eval (( 1_1 (J,F)),P)))) - (c * ((P . K) * (P . N)))) by A12, POLYNOM7: 29

          .= (((a * (p . i1)) - (b * (p . i2))) - ((c * (p . i3)) * (P . N))) by A10, A11;

          then (a * (p . i1)) = ((b * (p . i2)) + (((P . N) * c) * (p . i3))) by A9;

          hence s in D by A9;

        end;

        then D is diophantine;

        hence thesis;

      end;

    end;

    scheme :: HILB10_3:sch3

    IntersectionDiophantine { n() -> Nat , P,Q[ XFinSequence] } :

{ p where p be n() -element XFinSequence of NAT : P[p] & Q[p] } is diophantine Subset of (n() -xtuples_of NAT )

      provided

       A1: { p where p be n() -element XFinSequence of NAT : P[p] } is diophantine Subset of (n() -xtuples_of NAT )

       and

       A2: { p where p be n() -element XFinSequence of NAT : Q[p] } is diophantine Subset of (n() -xtuples_of NAT );

      reconsider PF = { p where p be n() -element XFinSequence of NAT : P[p] } as diophantine Subset of (n() -xtuples_of NAT ) by A1;

      reconsider QF = { p where p be n() -element XFinSequence of NAT : Q[p] } as diophantine Subset of (n() -xtuples_of NAT ) by A2;

      set PQ = { p where p be n() -element XFinSequence of NAT : P[p] & Q[p] };

      

       A3: (PF /\ QF) c= PQ

      proof

        let x be object;

        assume x in (PF /\ QF);

        then

         A4: x in PF & x in QF by XBOOLE_0:def 4;

        then

        consider p be n() -element XFinSequence of NAT such that

         A5: x = p & P[p];

        ex p be n() -element XFinSequence of NAT st x = p & Q[p] by A4;

        hence thesis by A5;

      end;

      

       A6: PQ c= PF

      proof

        let x be object;

        assume x in PQ;

        then ex p be n() -element XFinSequence of NAT st x = p & (P[p] & Q[p]);

        hence thesis;

      end;

      PQ c= QF

      proof

        let x be object;

        assume x in PQ;

        then ex p be n() -element XFinSequence of NAT st x = p & (P[p] & Q[p]);

        hence thesis;

      end;

      then PQ c= (PF /\ QF) by A6, XBOOLE_1: 19;

      hence thesis by A3, XBOOLE_0:def 10;

    end;

    scheme :: HILB10_3:sch4

    Substitution { P[ Nat, Nat, natural object, Nat, Nat, Nat], F( Nat, Nat, Nat) -> natural object } :

for i1, i2, i3, i4, i5 holds { p : P[(p . i1), (p . i2), F(.,.,.), (p . i3), (p . i4), (p . i5)] } is diophantine Subset of (n -xtuples_of NAT )

      provided

       A1: for i1, i2, i3, i4, i5, i6 holds { p : P[(p . i1), (p . i2), (p . i3), (p . i4), (p . i5), (p . i6)] } is diophantine Subset of (n -xtuples_of NAT )

       and

       A2: for i1, i2, i3, i4 holds { p : F(.,.,.) = (p . i4) } is diophantine Subset of (n -xtuples_of NAT );

      let n, i1, i2, i3, i4, i5;

      set n1 = (n + 1);

      set T = { p : P[(p . i1), (p . i2), F(.,.,.), (p . i3), (p . i4), (p . i5)] };

      per cases ;

        suppose

         A3: n = 0 ;

        T c= (n -xtuples_of NAT )

        proof

          let x be object;

          assume x in T;

          then ex p be n -element XFinSequence of NAT st x = p & P[(p . i1), (p . i2), F(.,.,.), (p . i3), (p . i4), (p . i5)];

          hence thesis by HILB10_2:def 5;

        end;

        hence thesis by A3;

      end;

        suppose

         A4: n <> 0 ;

        

         A5: n < n1 by NAT_1: 13;

        then n in ( Segm n1) by NAT_1: 44;

        then

        reconsider I1 = i1, I2 = i2, I3 = i3, I4 = i4, I5 = i5, N = n as Element of n1 by Th2;

        reconsider P = { p where p be n1 -element XFinSequence of NAT : P[(p . I1), (p . I2), (p . N), (p . I3), (p . I4), (p . I5)] } as diophantine Subset of (n1 -xtuples_of NAT ) by A1;

        reconsider F = { p where p be n1 -element XFinSequence of NAT : F(.,.,.) = (p . N) } as diophantine Subset of (n1 -xtuples_of NAT ) by A2;

        reconsider PF = (P /\ F) as Subset of (n1 -xtuples_of NAT );

        reconsider PFk = { (p | n) where p be n1 -element XFinSequence of NAT : p in PF } as diophantine Subset of (n -xtuples_of NAT ) by Th5, A5;

        

         A6: PFk c= T

        proof

          let x be object;

          assume x in PFk;

          then

          consider p be n1 -element XFinSequence of NAT such that

           A7: x = (p | n) & p in PF;

          p in P by A7, XBOOLE_0:def 4;

          then

           A8: ex q be n1 -element XFinSequence of NAT st p = q & P[(q . I1), (q . I2), (q . N), (q . I3), (q . I4), (q . I5)];

          p in F by A7, XBOOLE_0:def 4;

          then

           A9: ex q be n1 -element XFinSequence of NAT st p = q & F(.,.,.) = (q . N);

          ( len p) = n1 by CARD_1:def 7;

          then ( len (p | n)) = n by A5, AFINSQ_1: 54;

          then

          reconsider pn = (p | n) as n -element XFinSequence of NAT by CARD_1:def 7;

          (p . I1) = (pn . I1) & (p . I2) = (pn . I2) & (p . I3) = (pn . I3) & (p . I4) = (pn . I4) & (pn . I5) = (p . I5) by A4, Th4;

          hence thesis by A8, A9, A7;

        end;

        T c= PFk

        proof

          let x be object;

          assume x in T;

          then

          consider p be n -element XFinSequence of NAT such that

           A10: x = p & P[(p . i1), (p . i2), F(.,.,.), (p . i3), (p . i4), (p . i5)];

          reconsider FF = F(.,.,.) as Element of NAT by ORDINAL1:def 12;

          reconsider Z = <%FF%> as 1 -element XFinSequence of NAT ;

          set pZ = (p ^ Z);

          ( len p) = n by CARD_1:def 7;

          then

           A11: (pZ | n) = p & (pZ . n) = FF by AFINSQ_1: 57, AFINSQ_1: 36;

          then (p . i1) = (pZ . i1) & (p . i2) = (pZ . i2) & (p . i3) = (pZ . i3) & (p . i4) = (pZ . i4) & (p . i5) = (pZ . i5) by A4, Th4;

          then pZ in F & pZ in P by A10, A11;

          then pZ in (P /\ F) by XBOOLE_0:def 4;

          hence thesis by A11, A10;

        end;

        hence thesis by A6, XBOOLE_0:def 10;

      end;

    end;

    scheme :: HILB10_3:sch5

    SubstitutionInt { P[ Nat, Nat, Integer], F( Nat, Nat, Nat) -> Integer } :

for i1, i2, i3, i4, i5 holds { p : P[(p . i1), (p . i2), F(.,.,.)] } is diophantine Subset of (n -xtuples_of NAT )

      provided

       A1: for i1, i2, i3, a holds { p : P[(p . i1), (p . i2), (a * (p . i3))] } is diophantine Subset of (n -xtuples_of NAT )

       and

       A2: for i1, i2, i3, i4, a holds { p : F(.,.,.) = (a * (p . i4)) } is diophantine Subset of (n -xtuples_of NAT );

      deffunc AbsF( Nat, Nat, Nat) = |.F($1,$2,$3).|;

      defpred plusP[ Nat, Nat, natural object, Nat, Nat, Nat] means P[$1, $2, (1 * $3)] & F($4,$5,$6) >= 0 ;

      defpred minusP[ Nat, Nat, natural object, Nat, Nat, Nat] means P[$1, $2, (( - 1) * $3)] & F($4,$5,$6) <= 0 ;

      

       A3: for i1, i2, i3, i4, i5, i6 holds { p : plusP[(p . i1), (p . i2), (p . i3), (p . i4), (p . i5), (p . i6)] } is diophantine Subset of (n -xtuples_of NAT )

      proof

        let i1, i2, i3, i4, i5, i6;

        set M = { p : plusP[(p . i1), (p . i2), (p . i3), (p . i4), (p . i5), (p . i6)] };

        per cases ;

          suppose

           A4: n = 0 ;

          M c= (n -xtuples_of NAT )

          proof

            let x be object;

            assume x in M;

            then ex p be n -element XFinSequence of NAT st x = p & plusP[(p . i1), (p . i2), (p . i3), (p . i4), (p . i5), (p . i6)];

            hence thesis by HILB10_2:def 5;

          end;

          hence thesis by A4;

        end;

          suppose

           A5: n <> 0 ;

          set n1 = (n + 1);

          

           A6: n < n1 by NAT_1: 13;

          then n in ( Segm n1) by NAT_1: 44;

          then

          reconsider I1 = i1, I2 = i2, I3 = i3, I4 = i4, I5 = i5, I6 = i6, N = n as Element of n1 by Th2;

          defpred pP[ XFinSequence of NAT ] means P[($1 . I1), ($1 . I2), (1 * ($1 . I3))];

          reconsider P = { p where p be n1 -element XFinSequence of NAT : pP[p] } as diophantine Subset of (n1 -xtuples_of NAT ) by A1;

          reconsider F = { p where p be n1 -element XFinSequence of NAT : F(.,.,.) = (1 * (p . N)) } as diophantine Subset of (n1 -xtuples_of NAT ) by A2;

          reconsider PF = (P /\ F) as Subset of (n1 -xtuples_of NAT );

          reconsider PFk = { (p | n) where p be n1 -element XFinSequence of NAT : p in PF } as diophantine Subset of (n -xtuples_of NAT ) by Th5, A6;

          

           A7: PFk c= M

          proof

            let x be object;

            assume x in PFk;

            then

            consider p be n1 -element XFinSequence of NAT such that

             A8: x = (p | n) & p in PF;

            p in P by A8, XBOOLE_0:def 4;

            then

             A9: ex q be n1 -element XFinSequence of NAT st p = q & pP[q];

            p in F by A8, XBOOLE_0:def 4;

            then

             A10: ex q be n1 -element XFinSequence of NAT st p = q & F(.,.,.) = (1 * (q . N));

            ( len p) = n1 by CARD_1:def 7;

            then ( len (p | n)) = n by A6, AFINSQ_1: 54;

            then

            reconsider pn = (p | n) as n -element XFinSequence of NAT by CARD_1:def 7;

            (p . I1) = (pn . I1) & (p . I2) = (pn . I2) & (p . I3) = (pn . I3) & (p . I4) = (pn . I4) & (pn . I5) = (p . I5) & (pn . i6) = (p . I6) by A5, Th4;

            hence thesis by A8, A9, A10;

          end;

          M c= PFk

          proof

            let x be object;

            assume x in M;

            then

            consider p be n -element XFinSequence of NAT such that

             A11: x = p & plusP[(p . i1), (p . i2), (p . i3), (p . i4), (p . i5), (p . i6)];

            reconsider FF = F(.,.,.) as Element of NAT by A11, INT_1: 3;

            reconsider Z = <%FF%> as 1 -element XFinSequence of NAT ;

            set pZ = (p ^ Z);

            

             A12: ( len p) = n by CARD_1:def 7;

            then

             A13: (pZ | n) = p & (pZ . n) = FF by AFINSQ_1: 57, AFINSQ_1: 36;

            then (p . i1) = (pZ . i1) & (p . i2) = (pZ . i2) & (p . i3) = (pZ . i3) & (p . i4) = (pZ . i4) & (p . i5) = (pZ . i5) & (p . i6) = (pZ . i6) by A5, Th4;

            then F(.,.,.) = (1 * (pZ . n)) & P[(pZ . i1), (pZ . i2), (1 * (pZ . i3))] by A11, A12, AFINSQ_1: 36;

            then pZ in F & pZ in P;

            then pZ in (P /\ F) by XBOOLE_0:def 4;

            hence thesis by A13, A11;

          end;

          hence thesis by A7, XBOOLE_0:def 10;

        end;

      end;

      

       A14: for i1, i2, i3, i4, i5, i6 holds { p : minusP[(p . i1), (p . i2), (p . i3), (p . i4), (p . i5), (p . i6)] } is diophantine Subset of (n -xtuples_of NAT )

      proof

        let i1, i2, i3, i4, i5, i6;

        set M = { p : minusP[(p . i1), (p . i2), (p . i3), (p . i4), (p . i5), (p . i6)] };

        per cases ;

          suppose

           A15: n = 0 ;

          M c= (n -xtuples_of NAT )

          proof

            let x be object;

            assume x in M;

            then ex p be n -element XFinSequence of NAT st x = p & minusP[(p . i1), (p . i2), (p . i3), (p . i4), (p . i5), (p . i6)];

            hence thesis by HILB10_2:def 5;

          end;

          hence thesis by A15;

        end;

          suppose

           A16: n <> 0 ;

          set n1 = (n + 1);

          

           A17: n < n1 by NAT_1: 13;

          then n in ( Segm n1) by NAT_1: 44;

          then

          reconsider I1 = i1, I2 = i2, I3 = i3, I4 = i4, I5 = i5, I6 = i6, N = n as Element of n1 by Th2;

          defpred mP[ XFinSequence of NAT ] means P[($1 . I1), ($1 . I2), (( - 1) * ($1 . I3))];

          reconsider P = { p where p be n1 -element XFinSequence of NAT : mP[p] } as diophantine Subset of (n1 -xtuples_of NAT ) by A1;

          reconsider F = { p where p be n1 -element XFinSequence of NAT : F(.,.,.) = (( - 1) * (p . N)) } as diophantine Subset of (n1 -xtuples_of NAT ) by A2;

          reconsider PF = (P /\ F) as Subset of (n1 -xtuples_of NAT );

          reconsider PFk = { (p | n) where p be n1 -element XFinSequence of NAT : p in PF } as diophantine Subset of (n -xtuples_of NAT ) by Th5, A17;

          

           A18: PFk c= M

          proof

            let x be object;

            assume x in PFk;

            then

            consider p be n1 -element XFinSequence of NAT such that

             A19: x = (p | n) & p in PF;

            p in P by A19, XBOOLE_0:def 4;

            then

             A20: ex q be n1 -element XFinSequence of NAT st p = q & mP[q];

            p in F by A19, XBOOLE_0:def 4;

            then

             A21: ex q be n1 -element XFinSequence of NAT st p = q & F(.,.,.) = (( - 1) * (q . N));

            ( len p) = n1 by CARD_1:def 7;

            then ( len (p | n)) = n by A17, AFINSQ_1: 54;

            then

            reconsider pn = (p | n) as n -element XFinSequence of NAT by CARD_1:def 7;

            (p . I1) = (pn . I1) & (p . I2) = (pn . I2) & (p . I3) = (pn . I3) & (p . I4) = (pn . I4) & (pn . I5) = (p . I5) & (pn . i6) = (p . I6) by A16, Th4;

            hence thesis by A19, A20, A21;

          end;

          M c= PFk

          proof

            let x be object;

            assume x in M;

            then

            consider p be n -element XFinSequence of NAT such that

             A22: x = p & minusP[(p . i1), (p . i2), (p . i3), (p . i4), (p . i5), (p . i6)];

            reconsider FF = ( - F(.,.,.)) as Element of NAT by A22, INT_1: 3;

            reconsider Z = <%FF%> as 1 -element XFinSequence of NAT ;

            set pZ = (p ^ Z);

            ( len p) = n by CARD_1:def 7;

            then

             A23: (pZ | n) = p & (pZ . n) = FF by AFINSQ_1: 57, AFINSQ_1: 36;

            then (p . i1) = (pZ . i1) & (p . i2) = (pZ . i2) & (p . i3) = (pZ . i3) & (p . i4) = (pZ . i4) & (p . i5) = (pZ . i5) & (p . i6) = (pZ . i6) by A16, Th4;

            then F(.,.,.) = (( - 1) * (pZ . n)) & P[(pZ . i1), (pZ . i2), (( - 1) * (pZ . i3))] by A22, A23;

            then pZ in F & pZ in P;

            then pZ in (P /\ F) by XBOOLE_0:def 4;

            hence thesis by A23, A22;

          end;

          hence thesis by A18, XBOOLE_0:def 10;

        end;

      end;

      

       A24: for i1, i2, i3, i4 holds { p : AbsF(.,.,.) = (p . i4) } is diophantine Subset of (n -xtuples_of NAT )

      proof

        let i1, i2, i3, i4;

        defpred plusF[ XFinSequence of NAT ] means F(.,.,.) = (1 * ($1 . i4));

        defpred minusF[ XFinSequence of NAT ] means F(.,.,.) = (( - 1) * ($1 . i4));

        

         A25: { p : plusF[p] } is diophantine Subset of (n -xtuples_of NAT ) by A2;

        

         A26: { p : minusF[p] } is diophantine Subset of (n -xtuples_of NAT ) by A2;

        

         A27: { p : plusF[p] or minusF[p] } is diophantine Subset of (n -xtuples_of NAT ) from UnionDiophantine( A25, A26);

        defpred pmF[ XFinSequence of NAT ] means plusF[$1] or minusF[$1];

        defpred absF[ XFinSequence of NAT ] means AbsF(.,.,.) = ($1 . i4);

        

         A28: for p holds pmF[p] iff absF[p]

        proof

          let p;

          thus pmF[p] implies absF[p]

          proof

            assume

             A29: pmF[p];

            per cases by A29;

              suppose plusF[p];

              hence thesis by ABSVALUE:def 1;

            end;

              suppose minusF[p];

              then AbsF(.,.,.) = ( - (( - 1) * (p . i4))) by ABSVALUE: 30;

              hence thesis;

            end;

          end;

          assume

           A30: absF[p];

          per cases ;

            suppose F(.,.,.) >= 0 ;

            hence thesis by A30, ABSVALUE:def 1;

          end;

            suppose F(.,.,.) < 0 ;

            then AbsF(.,.,.) = ( - F(.,.,.)) by ABSVALUE:def 1;

            hence thesis by A30;

          end;

        end;

        { p : pmF[p] } = { q : absF[q] } from Eq( A28);

        hence thesis by A27;

      end;

      

       A31: for i1, i2, i3, i4, i5 holds { p : plusP[(p . i1), (p . i2), AbsF(.,.,.), (p . i3), (p . i4), (p . i5)] } is diophantine Subset of (n -xtuples_of NAT ) from Substitution( A3, A24);

      

       A32: for i1, i2, i3, i4, i5 holds { p : minusP[(p . i1), (p . i2), AbsF(.,.,.), (p . i3), (p . i4), (p . i5)] } is diophantine Subset of (n -xtuples_of NAT ) from Substitution( A14, A24);

      let n, i1, i2, i3, i4, i5;

      defpred pP[ XFinSequence of NAT ] means plusP[($1 . i1), ($1 . i2), AbsF(.,.,.), ($1 . i3), ($1 . i4), ($1 . i5)];

      defpred mP[ XFinSequence of NAT ] means minusP[($1 . i1), ($1 . i2), AbsF(.,.,.), ($1 . i3), ($1 . i4), ($1 . i5)];

      defpred pmP[ XFinSequence of NAT ] means pP[$1] or mP[$1];

      

       A33: { p : pP[p] } is diophantine Subset of (n -xtuples_of NAT ) by A31;

      

       A34: { p : mP[p] } is diophantine Subset of (n -xtuples_of NAT ) by A32;

      

       A35: { p : pP[p] or mP[p] } is diophantine Subset of (n -xtuples_of NAT ) from UnionDiophantine( A33, A34);

      defpred PF[ XFinSequence of NAT ] means P[($1 . i1), ($1 . i2), F(.,.,.)];

      

       A36: for p holds pmP[p] iff PF[p]

      proof

        let p;

        thus pmP[p] implies PF[p]

        proof

          assume

           A37: pP[p] or mP[p];

          per cases by A37;

            suppose pP[p];

            hence thesis by ABSVALUE:def 1;

          end;

            suppose

             A38: mP[p];

            then AbsF(.,.,.) = ( - F(.,.,.)) by ABSVALUE: 30;

            hence thesis by A38;

          end;

        end;

        assume

         A39: PF[p];

        per cases ;

          suppose F(.,.,.) >= 0 ;

          hence thesis by A39, ABSVALUE:def 1;

        end;

          suppose

           A40: F(.,.,.) < 0 ;

          then AbsF(.,.,.) = ( - F(.,.,.)) by ABSVALUE:def 1;

          hence thesis by A39, A40;

        end;

      end;

      { p : pmP[p] } = { q : PF[q] } from Eq( A36);

      hence thesis by A35;

    end;

    theorem :: HILB10_3:11

    

     Th11: for a, b, c, d, i1, i2, i3 holds { p : (a * (p . i1)) = (((b * (p . i2)) + (c * (p . i3))) + d) } is diophantine Subset of (n -xtuples_of NAT )

    proof

      let a,b,c,d be Integer, i1, i2, i3;

      set F = F_Real ;

      reconsider ar = a, br = b, cr = c, dr = d as integer Element of F by XREAL_0:def 1;

      set D = { p : (a * (p . i1)) = (((b * (p . i2)) + (c * (p . i3))) + d) };

      D c= (n -xtuples_of NAT )

      proof

        let y be object;

        assume y in D;

        then ex p st y = p & (a * (p . i1)) = (((b * (p . i2)) + (c * (p . i3))) + d);

        hence thesis by HILB10_2:def 5;

      end;

      then

      reconsider D as Subset of (n -xtuples_of NAT );

      per cases ;

        suppose n = 0 ;

        then D is diophantine Subset of (n -xtuples_of NAT );

        hence thesis;

      end;

        suppose

         A1: n <> 0 ;

        set Q = ((((ar * ( 1_1 (i1,F))) - (br * ( 1_1 (i2,F)))) - (cr * ( 1_1 (i3,F)))) - (dr * ( 1_ (n,F))));

        reconsider Q as INT -valued Polynomial of (n + 0 ), F_Real ;

        for s be object holds s in D iff ex x be n -element XFinSequence of NAT , y be 0 -element XFinSequence of NAT st s = x & ( eval (Q,( @ (x ^ y)))) = 0

        proof

          let s be object;

          thus s in D implies ex x be n -element XFinSequence of NAT , y be 0 -element XFinSequence of NAT st s = x & ( eval (Q,( @ (x ^ y)))) = 0

          proof

            assume s in D;

            then

            consider p such that

             A2: s = p & (a * (p . i1)) = (((b * (p . i2)) + (c * (p . i3))) + d);

            reconsider Z = ( <%> NAT ) as 0 -element XFinSequence of NAT ;

            take pZ = p, Z;

            

             A3: ( eval ((dr * ( 1_ (n,F))),( @ p))) = (dr * ( eval (( 1_ (n,F)),( @ p)))) by POLYNOM7: 29

            .= (dr * ( 1. F)) by POLYNOM2: 21

            .= d;

            

             A4: ( eval ((ar * ( 1_1 (i1,F))),( @ p))) = (ar * ( eval (( 1_1 (i1,F)),( @ p)))) by POLYNOM7: 29

            .= (a * (p . i1)) by A1, Th1;

            

             A5: ( eval ((br * ( 1_1 (i2,F))),( @ p))) = (br * ( eval (( 1_1 (i2,F)),( @ p)))) by POLYNOM7: 29

            .= (b * (p . i2)) by A1, Th1;

            

             A6: ( eval ((cr * ( 1_1 (i3,F))),( @ p))) = (cr * ( eval (( 1_1 (i3,F)),( @ p)))) by POLYNOM7: 29

            .= (c * (p . i3)) by A1, Th1;

            ( eval (Q,( @ (p ^ Z)))) = (( eval ((((ar * ( 1_1 (i1,F))) - (br * ( 1_1 (i2,F)))) - (cr * ( 1_1 (i3,F)))),( @ p))) - ( eval ((dr * ( 1_ (n,F))),( @ p)))) by POLYNOM2: 24

            .= ((( eval (((ar * ( 1_1 (i1,F))) - (br * ( 1_1 (i2,F)))),( @ p))) - ( eval ((cr * ( 1_1 (i3,F))),( @ p)))) - ( eval ((dr * ( 1_ (n,F))),( @ p)))) by POLYNOM2: 24

            .= (((( eval ((ar * ( 1_1 (i1,F))),( @ p))) - ( eval ((br * ( 1_1 (i2,F))),( @ p)))) - ( eval ((cr * ( 1_1 (i3,F))),( @ p)))) - ( eval ((dr * ( 1_ (n,F))),( @ p)))) by POLYNOM2: 24

            .= 0 by A2, A3, A4, A5, A6;

            hence thesis by A2;

          end;

          given p be n -element XFinSequence of NAT , Z be 0 -element XFinSequence of NAT such that

           A7: s = p & ( eval (Q,( @ (p ^ Z)))) = 0 ;

          

           A8: ( eval ((dr * ( 1_ (n,F))),( @ p))) = (dr * ( eval (( 1_ (n,F)),( @ p)))) by POLYNOM7: 29

          .= (dr * ( 1. F)) by POLYNOM2: 21

          .= d;

          

           A9: ( eval ((ar * ( 1_1 (i1,F))),( @ p))) = (ar * ( eval (( 1_1 (i1,F)),( @ p)))) by POLYNOM7: 29

          .= (a * (p . i1)) by A1, Th1;

          

           A10: ( eval ((br * ( 1_1 (i2,F))),( @ p))) = (br * ( eval (( 1_1 (i2,F)),( @ p)))) by POLYNOM7: 29

          .= (b * (p . i2)) by A1, Th1;

          

           A11: ( eval ((cr * ( 1_1 (i3,F))),( @ p))) = (cr * ( eval (( 1_1 (i3,F)),( @ p)))) by POLYNOM7: 29

          .= (c * (p . i3)) by A1, Th1;

          ( eval (Q,( @ (p ^ Z)))) = (( eval ((((ar * ( 1_1 (i1,F))) - (br * ( 1_1 (i2,F)))) - (cr * ( 1_1 (i3,F)))),( @ p))) - ( eval ((dr * ( 1_ (n,F))),( @ p)))) by POLYNOM2: 24

          .= ((( eval (((ar * ( 1_1 (i1,F))) - (br * ( 1_1 (i2,F)))),( @ p))) - ( eval ((cr * ( 1_1 (i3,F))),( @ p)))) - ( eval ((dr * ( 1_ (n,F))),( @ p)))) by POLYNOM2: 24

          .= (((( eval ((ar * ( 1_1 (i1,F))),( @ p))) - ( eval ((br * ( 1_1 (i2,F))),( @ p)))) - ( eval ((cr * ( 1_1 (i3,F))),( @ p)))) - ( eval ((dr * ( 1_ (n,F))),( @ p)))) by POLYNOM2: 24

          .= ((((a * (p . i1)) - (b * (p . i2))) - (c * (p . i3))) - d) by A8, A9, A10, A11;

          then (a * (p . i1)) = (((b * (p . i2)) + (c * (p . i3))) + d) by A7;

          hence thesis by A7;

        end;

        then D is diophantine;

        hence thesis;

      end;

    end;

    theorem :: HILB10_3:12

    

     Th12: for a, i1, i2 holds { p : (p . i1) = (a * (p . i2)) } is diophantine Subset of (n -xtuples_of NAT )

    proof

      let a be Integer, i1, i2;

      defpred P[ XFinSequence of NAT ] means ($1 . i1) = (a * ($1 . i2));

      defpred Q[ XFinSequence of NAT ] means (1 * ($1 . i1)) = ((a * ($1 . i2)) + 0 );

      

       A1: { p : (p . i1) = (a * (p . i2)) } c= { q : (1 * (q . i1)) = ((a * (q . i2)) + 0 ) }

      proof

        let y be object;

        assume y in { p : (p . i1) = (a * (p . i2)) };

        then

        consider p be n -element XFinSequence of NAT such that

         A2: y = p & (p . i1) = (a * (p . i2));

        (1 * (p . i1)) = ((a * (p . i2)) + 0 ) by A2;

        hence thesis by A2;

      end;

      { q : (1 * (q . i1)) = ((a * (q . i2)) + 0 ) } c= { p : (p . i1) = (a * (p . i2)) }

      proof

        let y be object;

        assume y in { q : (1 * (q . i1)) = ((a * (q . i2)) + 0 ) };

        then ex q be n -element XFinSequence of NAT st y = q & (1 * (q . i1)) = ((a * (q . i2)) + 0 );

        hence thesis;

      end;

      then { q : (1 * (q . i1)) = ((a * (q . i2)) + 0 ) } = { p : (p . i1) = (a * (p . i2)) } by A1, XBOOLE_0:def 10;

      hence thesis by Th6;

    end;

    theorem :: HILB10_3:13

    

     Th13: for a, b, i1 holds { p : (a * (p . i1)) = b } is diophantine Subset of (n -xtuples_of NAT )

    proof

      let a,b be Integer, i1;

      set i2 = the Element of n;

      defpred P[ XFinSequence of NAT ] means (a * ($1 . i1)) = b;

      defpred Q[ XFinSequence of NAT ] means (a * ($1 . i1)) = (( 0 * ($1 . i2)) + b);

      

       A1: for p holds P[p] iff Q[p];

      { p : P[p] } = { q : Q[q] } from Eq( A1);

      hence thesis by Th6;

    end;

    theorem :: HILB10_3:14

    

     Th14: for a, i1 holds { p : (p . i1) = a } is diophantine Subset of (n -xtuples_of NAT )

    proof

      let a be Integer, i1;

      set i2 = the Element of n;

      defpred P[ XFinSequence of NAT ] means ($1 . i1) = a;

      defpred Q[ XFinSequence of NAT ] means (1 * ($1 . i1)) = (( 0 * ($1 . i2)) + a);

      

       A1: for p holds P[p] iff Q[p];

      { p : P[p] } = { q : Q[q] } from Eq( A1);

      hence thesis by Th6;

    end;

    theorem :: HILB10_3:15

    for a, b, i1, i2 holds { p : (p . i1) = ((a * (p . i2)) + b) } is diophantine Subset of (n -xtuples_of NAT )

    proof

      let a,b be Integer, i1, i2;

      defpred P[ XFinSequence of NAT ] means ($1 . i1) = ((a * ($1 . i2)) + b);

      defpred Q[ XFinSequence of NAT ] means (1 * ($1 . i1)) = ((a * ($1 . i2)) + b);

      

       A1: for p holds P[p] iff Q[p];

      { p : P[p] } = { q : Q[q] } from Eq( A1);

      hence thesis by Th6;

    end;

    theorem :: HILB10_3:16

    for a, b, c, i1, i2 holds { p : (a * (p . i1)) <> ((b * (p . i2)) + c) } is diophantine Subset of (n -xtuples_of NAT )

    proof

      let a,b,c be Integer, i1, i2;

      defpred P[ XFinSequence of NAT ] means (a * ($1 . i1)) > ((b * ($1 . i2)) + c);

      defpred Q[ XFinSequence of NAT ] means ((a * ($1 . i1)) + ( - c)) < (b * ($1 . i2));

      defpred R[ XFinSequence of NAT ] means P[$1] or Q[$1];

      defpred S[ XFinSequence of NAT ] means (a * ($1 . i1)) <> ((b * ($1 . i2)) + c);

      

       A1: { p : P[p] } is diophantine Subset of (n -xtuples_of NAT ) by Th7;

      

       A2: { p : Q[p] } is diophantine Subset of (n -xtuples_of NAT ) by Th7;

      

       A3: { p : P[p] or Q[p] } is diophantine Subset of (n -xtuples_of NAT ) from UnionDiophantine( A1, A2);

      

       A4: R[p] iff S[p]

      proof

        thus R[p] implies S[p];

        assume S[p];

        then (a * (p . i1)) > ((b * (p . i2)) + c) or (a * (p . i1)) < ((b * (p . i2)) + c) by XXREAL_0: 1;

        then (a * (p . i1)) > ((b * (p . i2)) + c) or ((a * (p . i1)) - c) < (b * (p . i2)) by XREAL_1: 19;

        hence thesis;

      end;

      { p : R[p] } = { q : S[q] } from Eq( A4);

      hence thesis by A3;

    end;

    theorem :: HILB10_3:17

    

     Th17: for a, b, i1, i2, i3 holds { p : (a * (p . i1)) > ((b * (p . i2)) * (p . i3)) } is diophantine Subset of (n -xtuples_of NAT )

    proof

      let a, b, i1, i2, i3;

      defpred P[ Nat, Nat, Integer] means (a * $1) > ($3 + 0 );

      deffunc F( Nat, Nat, Nat) = ((b * $2) * $3);

      defpred P1[ XFinSequence of NAT ] means (a * ($1 . i1)) > (((b * ($1 . i2)) * ($1 . i3)) + 0 );

      defpred P2[ XFinSequence of NAT ] means (a * ($1 . i1)) > ((b * ($1 . i2)) * ($1 . i3));

      

       A1: for n holds for i1, i2, i3, c holds { p : P[(p . i1), (p . i2), (c * (p . i3))] } is diophantine Subset of (n -xtuples_of NAT ) by Th7;

      

       A2: for n holds for i1, i2, i3, i4, c holds { p : F(.,.,.) = (c * (p . i4)) } is diophantine Subset of (n -xtuples_of NAT ) by Th9;

      

       A3: for n holds for i1, i2, i3, i4, i5 holds { p : P[(p . i1), (p . i2), F(.,.,.)] } is diophantine Subset of (n -xtuples_of NAT ) from SubstitutionInt( A1, A2);

      

       A4: for p holds P1[p] iff P2[p];

      { p : P1[p] } = { q : P2[q] } from Eq( A4);

      hence thesis by A3;

    end;

    theorem :: HILB10_3:18

    

     Th18: for a, b, c, i1, i2, i3 holds { p : (a * (p . i1)) < ((b * (p . i2)) + (c * (p . i3))) } is diophantine Subset of (n -xtuples_of NAT )

    proof

      let a, b, c, i1, i2, i3;

      defpred P[ Nat, Nat, Integer] means ((a * $1) + 0 ) < $3;

      deffunc F( Nat, Nat, Nat) = (((b * $2) + (c * $3)) + 0 );

      defpred P1[ XFinSequence of NAT ] means ((a * ($1 . i1)) + 0 ) < (((b * ($1 . i2)) + (c * ($1 . i3))) + 0 );

      defpred P2[ XFinSequence of NAT ] means (a * ($1 . i1)) < ((b * ($1 . i2)) + (c * ($1 . i3)));

      

       A1: for n holds for i1, i2, i3, d holds { p : P[(p . i1), (p . i2), (d * (p . i3))] } is diophantine Subset of (n -xtuples_of NAT ) by Th7;

      

       A2: for n holds for i1, i2, i3, i4, d holds { p : F(.,.,.) = (d * (p . i4)) } is diophantine Subset of (n -xtuples_of NAT ) by Th11;

      

       A3: for n holds for i1, i2, i3, i4, i5 holds { p : P[(p . i1), (p . i2), F(.,.,.)] } is diophantine Subset of (n -xtuples_of NAT ) from SubstitutionInt( A1, A2);

      

       A4: for p holds P1[p] iff P2[p];

      { p : P1[p] } = { q : P2[q] } from Eq( A4);

      hence thesis by A3;

    end;

    theorem :: HILB10_3:19

    

     Th19: for a, b, c, i1, i2, i3 holds { p : (a * (p . i1)) = ((b * (p . i2)) -' (c * (p . i3))) } is diophantine Subset of (n -xtuples_of NAT )

    proof

      let a,b,c be Integer, i1, i2, i3;

      defpred P[ XFinSequence of NAT ] means (a * ($1 . i1)) = (((b * ($1 . i2)) + (( - c) * ($1 . i3))) + 0 );

      defpred Q[ XFinSequence of NAT ] means (b * ($1 . i2)) >= ((c * ($1 . i3)) + 0 );

      defpred R[ XFinSequence of NAT ] means (a * ($1 . i1)) = (( 0 * ($1 . i2)) * ($1 . i3));

      defpred S[ XFinSequence of NAT ] means ((b * ($1 . i2)) + 0 ) < (c * ($1 . i3));

      defpred PQ[ XFinSequence of NAT ] means P[$1] & Q[$1];

      

       A1: { p : P[p] } is diophantine Subset of (n -xtuples_of NAT ) by Th11;

      

       A2: { p : Q[p] } is diophantine Subset of (n -xtuples_of NAT ) by Th8;

      { p : P[p] & Q[p] } is diophantine Subset of (n -xtuples_of NAT ) from IntersectionDiophantine( A1, A2);

      then

       A3: { p : PQ[p] } is diophantine Subset of (n -xtuples_of NAT );

      defpred RS[ XFinSequence of NAT ] means R[$1] & S[$1];

      

       A4: { p : R[p] } is diophantine Subset of (n -xtuples_of NAT ) by Th9;

      

       A5: { p : S[p] } is diophantine Subset of (n -xtuples_of NAT ) by Th7;

      { p : R[p] & S[p] } is diophantine Subset of (n -xtuples_of NAT ) from IntersectionDiophantine( A4, A5);

      then

       A6: { p : RS[p] } is diophantine Subset of (n -xtuples_of NAT );

      defpred PQRS[ XFinSequence of NAT ] means PQ[$1] or RS[$1];

      defpred T[ XFinSequence of NAT ] means (a * ($1 . i1)) = ((b * ($1 . i2)) -' (c * ($1 . i3)));

      

       A7: { p : PQ[p] or RS[p] } is diophantine Subset of (n -xtuples_of NAT ) from UnionDiophantine( A3, A6);

      

       A8: PQRS[p] iff T[p]

      proof

        thus PQRS[p] implies T[p]

        proof

          assume PQRS[p];

          then ((a * (p . i1)) = (((b * (p . i2)) + (( - c) * (p . i3))) + 0 ) & ((b * (p . i2)) - (c * (p . i3))) >= 0 ) or ((a * (p . i1)) = (( 0 * (p . i2)) * (p . i3)) & ((b * (p . i2)) - (c * (p . i3))) < 0 ) by XREAL_1: 48, XREAL_1: 49;

          hence thesis by XREAL_0:def 2;

        end;

        assume T[p];

        then ((a * (p . i1)) = (((b * (p . i2)) - (c * (p . i3))) + 0 ) & ((b * (p . i2)) - (c * (p . i3))) >= 0 ) or ((a * (p . i1)) = 0 & ((b * (p . i2)) - (c * (p . i3))) < 0 ) by XREAL_0:def 2;

        hence thesis by XREAL_1: 48, XREAL_1: 49;

      end;

      { p : PQRS[p] } = { q : T[q] } from Eq( A8);

      hence thesis by A7;

    end;

    theorem :: HILB10_3:20

    

     Th20: for a, b, c, i1, i2, i3 holds { p : (a * (p . i1)) = ((b * (p . i2)) -' c) } is diophantine Subset of (n -xtuples_of NAT )

    proof

      let a, b, c;

      defpred P[ Nat, Nat, Integer] means (a * $1) = ((b * $2) -' $3);

      

       A1: for n holds for i1, i2, i3, d holds { p : P[(p . i1), (p . i2), (d * (p . i3))] } is diophantine Subset of (n -xtuples_of NAT ) by Th19;

      deffunc F( Nat, Nat, Nat) = c;

      

       A2: for n holds for i1, i2, i3, i4, d holds { p : F(.,.,.) = (d * (p . i4)) } is diophantine Subset of (n -xtuples_of NAT ) by Th13;

      for n holds for i1, i2, i3, i4, i5 holds { p : P[(p . i1), (p . i2), F(.,.,.)] } is diophantine Subset of (n -xtuples_of NAT ) from SubstitutionInt( A1, A2);

      hence thesis;

    end;

    

     Lm1: for x,y be Integer holds for 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;

      let 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_3:21

    

     Th21: for a, b, c, i1, i2, i3 holds { p : ((a * (p . i1)),(b * (p . i2))) are_congruent_mod (c * (p . i3)) } is diophantine Subset of (n -xtuples_of NAT )

    proof

      let a, b, c, i1, i2, i3;

      defpred P[ XFinSequence of NAT ] means ex z be Nat st (a * ($1 . i1)) = ((b * ($1 . i2)) + ((z * c) * ($1 . i3)));

      defpred Q[ XFinSequence of NAT ] means ex z be Nat st (b * ($1 . i2)) = ((a * ($1 . i1)) + ((z * c) * ($1 . i3)));

      

       A1: { p : P[p] } is diophantine Subset of (n -xtuples_of NAT ) by Th10;

      

       A2: { p : Q[p] } is diophantine Subset of (n -xtuples_of NAT ) by Th10;

      

       A3: { p : P[p] or Q[p] } is diophantine Subset of (n -xtuples_of NAT ) from UnionDiophantine( A1, A2);

      set PP = { p : ((a * (p . i1)),(b * (p . i2))) are_congruent_mod (c * (p . i3)) };

      

       A4: PP c= { p : P[p] or Q[p] }

      proof

        let x be object;

        assume x in PP;

        then

        consider p such that

         A5: x = p & ((a * (p . i1)),(b * (p . i2))) are_congruent_mod (c * (p . i3));

        consider i be Integer such that

         A6: ((c * (p . i3)) * i) = ((a * (p . i1)) - (b * (p . i2))) by A5, INT_1:def 5;

        per cases ;

          suppose i >= 0 ;

          then

          reconsider i as Element of NAT by INT_1: 3;

          (a * (p . i1)) = ((b * (p . i2)) + ((i * c) * (p . i3))) by A6;

          hence thesis by A5;

        end;

          suppose i < 0 ;

          then

          reconsider I = ( - i) as Element of NAT by INT_1: 3;

          

           A7: (a * (p . i1)) = ((b * (p . i2)) + ((i * c) * (p . i3))) by A6;

          (a * (p . i1)) = ((b * (p . i2)) + ((( - I) * c) * (p . i3))) by A7;

          then (b * (p . i2)) = ((a * (p . i1)) + ((I * c) * (p . i3)));

          hence thesis by A5;

        end;

      end;

      { p : P[p] or Q[p] } c= PP

      proof

        let x be object;

        assume x in { p : P[p] or Q[p] };

        then

        consider p such that

         A8: x = p & ( P[p] or Q[p]);

        per cases by A8;

          suppose P[p];

          then

          consider z be Nat such that

           A9: (a * (p . i1)) = ((b * (p . i2)) + ((z * c) * (p . i3)));

          (z * (c * (p . i3))) = ((a * (p . i1)) - (b * (p . i2))) by A9;

          then ((a * (p . i1)),(b * (p . i2))) are_congruent_mod (c * (p . i3)) by INT_1:def 5;

          hence x in PP by A8;

        end;

          suppose Q[p];

          then

          consider z be Nat such that

           A10: (b * (p . i2)) = ((a * (p . i1)) + ((z * c) * (p . i3)));

          (( - z) * (c * (p . i3))) = ((a * (p . i1)) - (b * (p . i2))) by A10;

          then ((a * (p . i1)),(b * (p . i2))) are_congruent_mod (c * (p . i3)) by INT_1:def 5;

          hence x in PP by A8;

        end;

      end;

      hence thesis by A3, A4, XBOOLE_0:def 10;

    end;

    theorem :: HILB10_3:22

    

     Th22: for a, b, c, i1, i2, i3 holds { p : [(a * (p . i1)), (b * (p . i2))] is Pell's_solution of (((c * (p . i3)) ^2 ) -' 1) } is diophantine Subset of (n -xtuples_of NAT )

    proof

      let a,b,c be Integer;

      let i1, i2, i3;

      set n5 = (n + 5);

      set WW = { p : [(a * (p . i1)), (b * (p . i2))] is Pell's_solution of (((c * (p . i3)) ^2 ) -' 1) };

      WW c= (n -xtuples_of NAT )

      proof

        let y be object;

        assume y in WW;

        then ex p st y = p & [(a * (p . i1)), (b * (p . i2))] is Pell's_solution of (((c * (p . i3)) ^2 ) -' 1);

        hence thesis by HILB10_2:def 5;

      end;

      then

      reconsider WW as Subset of (n -xtuples_of NAT );

      per cases ;

        suppose n = 0 ;

        then WW is diophantine Subset of (n -xtuples_of NAT );

        hence thesis;

      end;

        suppose

         A1: n <> 0 ;

        n = (n + 0 );

        then

        reconsider N = n, I1 = i1, I2 = i2, I3 = i3, N1 = (n + 1), N2 = (n + 2), N3 = (n + 3), N4 = (n + 4) as Element of (n + 5) by Th2, Th3;

        defpred P[ XFinSequence of NAT ] means (1 * ($1 . N)) = (((a ^2 ) * ($1 . I1)) * ($1 . I1));

        

         A2: { p where p be (n + 5) -element XFinSequence of NAT : P[p] } is diophantine Subset of (n5 -xtuples_of NAT ) by Th9;

        defpred Q[ XFinSequence of NAT ] means (1 * ($1 . N1)) = (((c ^2 ) * ($1 . I3)) * ($1 . I3));

        

         A3: { p where p be (n + 5) -element XFinSequence of NAT : Q[p] } is diophantine Subset of (n5 -xtuples_of NAT ) by Th9;

        defpred R[ XFinSequence of NAT ] means (1 * ($1 . N2)) = ((1 * ($1 . N1)) -' 1);

        

         A4: { p where p be (n + 5) -element XFinSequence of NAT : R[p] } is diophantine Subset of (n5 -xtuples_of NAT ) by Th20;

        defpred S[ XFinSequence of NAT ] means (1 * ($1 . N3)) = (((b ^2 ) * ($1 . I2)) * ($1 . I2));

        

         A5: { p where p be (n + 5) -element XFinSequence of NAT : S[p] } is diophantine Subset of (n5 -xtuples_of NAT ) by Th9;

        defpred T[ XFinSequence of NAT ] means (1 * ($1 . N4)) = ((1 * ($1 . N2)) * ($1 . N3));

        

         A6: { p where p be (n + 5) -element XFinSequence of NAT : T[p] } is diophantine Subset of (n5 -xtuples_of NAT ) by Th9;

        defpred U[ XFinSequence of NAT ] means (1 * ($1 . N)) = ((1 * ($1 . N4)) + 1);

        

         A7: { p where p be (n + 5) -element XFinSequence of NAT : U[p] } is diophantine Subset of (n5 -xtuples_of NAT ) by Th6;

        defpred PQ[ XFinSequence of NAT ] means P[$1] & Q[$1];

        defpred PQR[ XFinSequence of NAT ] means PQ[$1] & R[$1];

        defpred PQRS[ XFinSequence of NAT ] means PQR[$1] & S[$1];

        defpred PQRST[ XFinSequence of NAT ] means PQRS[$1] & T[$1];

        defpred PQRSTU[ XFinSequence of NAT ] means PQRST[$1] & U[$1];

        { p where p be (n + 5) -element XFinSequence of NAT : P[p] & Q[p] } is diophantine Subset of (n5 -xtuples_of NAT ) from IntersectionDiophantine( A2, A3);

        then

         A8: { p where p be (n + 5) -element XFinSequence of NAT : PQ[p] } is diophantine Subset of (n5 -xtuples_of NAT );

        { p where p be (n + 5) -element XFinSequence of NAT : PQ[p] & R[p] } is diophantine Subset of ((n + 5) -xtuples_of NAT ) from IntersectionDiophantine( A8, A4);

        then

         A9: { p where p be (n + 5) -element XFinSequence of NAT : PQR[p] } is diophantine Subset of (n5 -xtuples_of NAT );

        { p where p be (n + 5) -element XFinSequence of NAT : PQR[p] & S[p] } is diophantine Subset of (n5 -xtuples_of NAT ) from IntersectionDiophantine( A9, A5);

        then

         A10: { p where p be (n + 5) -element XFinSequence of NAT : PQRS[p] } is diophantine Subset of (n5 -xtuples_of NAT );

        { p where p be (n + 5) -element XFinSequence of NAT : PQRS[p] & T[p] } is diophantine Subset of (n5 -xtuples_of NAT ) from IntersectionDiophantine( A10, A6);

        then

         A11: { p where p be (n + 5) -element XFinSequence of NAT : PQRST[p] } is diophantine Subset of (n5 -xtuples_of NAT );

        

         A12: { p where p be (n + 5) -element XFinSequence of NAT : PQRST[p] & U[p] } is diophantine Subset of (n5 -xtuples_of NAT ) from IntersectionDiophantine( A11, A7);

        set DD = { p where p be (n + 5) -element XFinSequence of NAT : PQRSTU[p] };

        set DDR = { (p | n) where p be (n + 5) -element XFinSequence of NAT : p in DD };

        

         A13: DDR is diophantine Subset of (n -xtuples_of NAT ) by NAT_1: 11, Th5, A12;

        

         A14: DDR c= WW

        proof

          let x be object such that

           A15: x in DDR;

          consider p be (n + 5) -element XFinSequence of NAT such that

           A16: x = (p | n) & p in DD by A15;

          consider q be (n + 5) -element XFinSequence of NAT such that

           A17: p = q & PQRSTU[q] by A16;

          ( len p) = (n + 5) & (n + 5) >= n by CARD_1:def 7, NAT_1: 11;

          then ( len (p | n)) = n by AFINSQ_1: 54;

          then

          reconsider pn = (p | n) as n -element XFinSequence of NAT by CARD_1:def 7;

          

           A18: (((b ^2 ) * (p . I2)) * (p . I2)) = ((b ^2 ) * ((p . I2) * (p . I2))) = ((b ^2 ) * ((p . I2) ^2 )) = ((b * (p . I2)) ^2 ) by SQUARE_1:def 1, SQUARE_1: 9;

          

           A19: (((a ^2 ) * (p . I1)) * (p . I1)) = ((a ^2 ) * ((p . I1) * (p . I1))) = ((a ^2 ) * ((p . I1) ^2 )) = ((a * (p . I1)) ^2 ) by SQUARE_1:def 1, SQUARE_1: 9;

          

           A20: (((c ^2 ) * (p . I3)) * (p . I3)) = ((c ^2 ) * ((p . I3) * (p . I3))) = ((c ^2 ) * ((p . I3) ^2 )) = ((c * (p . I3)) ^2 ) by SQUARE_1:def 1, SQUARE_1: 9;

          

           A21: ((p | n) . I3) = (p . i3) & ((p | n) . I2) = (p . i2) & ((p | n) . I1) = (p . i1) by A1, Th4;

          ((a * (pn . i1)) ^2 ) = (((((c * (pn . i3)) ^2 ) -' 1) * ((b * (pn . i2)) ^2 )) + 1) by A17, A18, A19, A20, A21;

          then (((a * (pn . i1)) ^2 ) - ((((c * (pn . i3)) ^2 ) -' 1) * ((b * (pn . i2)) ^2 ))) = 1;

          then [(a * (pn . i1)), (b * (pn . i2))] is Pell's_solution of (((c * (pn . i3)) ^2 ) -' 1) by Lm1;

          hence thesis by A16;

        end;

        WW c= DDR

        proof

          let x be object such that

           A22: x in WW;

          consider p be n -element XFinSequence of NAT such that

           A23: x = p & [(a * (p . i1)), (b * (p . i2))] is Pell's_solution of (((c * (p . i3)) ^2 ) -' 1) by A22;

          

           A24: ((a * (p . i1)) ^2 ) = ((a ^2 ) * ((p . i1) ^2 )) = ((a ^2 ) * ((p . i1) * (p . i1))) = (((a ^2 ) * (p . i1)) * (p . i1)) by SQUARE_1:def 1, SQUARE_1: 9;

          

           A25: ((b * (p . i2)) ^2 ) = ((b ^2 ) * ((p . i2) ^2 )) = ((b ^2 ) * ((p . i2) * (p . i2))) = (((b ^2 ) * (p . i2)) * (p . i2)) by SQUARE_1:def 1, SQUARE_1: 9;

          

           A26: ((c * (p . i3)) ^2 ) = ((c ^2 ) * ((p . i3) ^2 )) = ((c ^2 ) * ((p . i3) * (p . i3))) = (((c ^2 ) * (p . i3)) * (p . i3)) by SQUARE_1:def 1, SQUARE_1: 9;

          set y1 = (((a ^2 ) * (p . i1)) * (p . i1));

          set y2 = (((c ^2 ) * (p . i3)) * (p . i3));

          set y3 = ((1 * y2) -' 1);

          set y4 = (((b ^2 ) * (p . i2)) * (p . i2));

          set y5 = ((1 * y3) * y4);

          reconsider y1, y2, y3, y4, y5 as Element of NAT by ORDINAL1:def 12;

          set Y = (((( <%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>);

          set PY = (p ^ Y);

          

           A27: ( len p) = n & ( len Y) = 5 by CARD_1:def 7;

          

           A28: (PY | n) = p by A27, AFINSQ_1: 57;

          

           A29: (PY . i1) = (p . i1) by A28, A1, Th4;

          

           A30: (PY . i2) = ((PY | n) . i2) by A1, Th4

          .= (p . i2) by A27, AFINSQ_1: 57;

          

           A31: (PY . i3) = ((PY | n) . i3) by A1, Th4

          .= (p . i3) by A27, AFINSQ_1: 57;

           0 in ( dom Y) by A27, AFINSQ_1: 66;

          

          then

           A32: (PY . (n + 0 )) = (Y . 0 ) by A27, AFINSQ_1:def 3

          .= y1 by AFINSQ_1: 46;

          1 in ( dom Y) by A27, AFINSQ_1: 66;

          

          then

           A33: (PY . (n + 1)) = (Y . 1) by A27, AFINSQ_1:def 3

          .= y2 by AFINSQ_1: 46;

          2 in ( dom Y) by A27, AFINSQ_1: 66;

          

          then

           A34: (PY . (n + 2)) = (Y . 2) by A27, AFINSQ_1:def 3

          .= y3 by AFINSQ_1: 46;

          3 in ( dom Y) by A27, AFINSQ_1: 66;

          

          then

           A35: (PY . (n + 3)) = (Y . 3) by A27, AFINSQ_1:def 3

          .= y4 by AFINSQ_1: 46;

          4 in ( dom Y) by A27, AFINSQ_1: 66;

          

          then

           A36: (PY . (n + 4)) = (Y . 4) by A27, AFINSQ_1:def 3

          .= y5 by AFINSQ_1: 46;

          (y1 - y5) = 1 by A23, Lm1, A24, A25, A26;

          then y1 = (y5 + 1);

          then PQRSTU[PY] by A32, A31, A33, A29, A34, A35, A30, A36;

          then PY in DD;

          hence thesis by A23, A28;

        end;

        hence thesis by A13, A14, XBOOLE_0:def 10;

      end;

    end;

    begin

    theorem :: HILB10_3:23

    

     Th23: for i1, i2, i3 holds { p : (p . i1) = ( Py ((p . i2),(p . i3))) & (p . i2) > 1 } is diophantine Subset of (n -xtuples_of NAT )

    proof

      let i1, i2, i3;

      set n9 = (n + 9);

      set WW = { p : (p . i1) = ( Py ((p . i2),(p . i3))) & (p . i2) > 1 };

      WW c= (n -xtuples_of NAT )

      proof

        let y be object;

        assume y in WW;

        then ex p st y = p & (p . i1) = ( Py ((p . i2),(p . i3))) & (p . i2) > 1;

        hence thesis by HILB10_2:def 5;

      end;

      then

      reconsider WW as Subset of (n -xtuples_of NAT );

      per cases ;

        suppose n = 0 ;

        then WW is diophantine Subset of (n -xtuples_of NAT );

        hence thesis;

      end;

        suppose

         A1: n <> 0 ;

        n = (n + 0 );

        then

        reconsider N = n, I1 = i1, I2 = i2, I3 = i3, N1 = (n + 1), N2 = (n + 2), N3 = (n + 3), N4 = (n + 4), N5 = (n + 5), N6 = (n + 6), N7 = (n + 7), N8 = (n + 8) as Element of n9 by Th2, Th3;

        defpred P0[ XFinSequence of NAT ] means (1 * ($1 . I2)) > (( 0 * ($1 . I1)) + 1);

        

         A2: { p where p be n9 -element XFinSequence of NAT : P0[p] } is diophantine Subset of (n9 -xtuples_of NAT ) by Th7;

        defpred P1[ XFinSequence of NAT ] means [(1 * ($1 . N)), (1 * ($1 . I1))] is Pell's_solution of (((1 * ($1 . I2)) ^2 ) -' 1);

        

         A3: { p where p be n9 -element XFinSequence of NAT : P1[p] } is diophantine Subset of (n9 -xtuples_of NAT ) by Th22;

        defpred P2[ XFinSequence of NAT ] means [(1 * ($1 . N1)), (1 * ($1 . N2))] is Pell's_solution of (((1 * ($1 . I2)) ^2 ) -' 1);

        

         A4: { p where p be n9 -element XFinSequence of NAT : P2[p] } is diophantine Subset of (n9 -xtuples_of NAT ) by Th22;

        defpred P3[ XFinSequence of NAT ] means (1 * ($1 . N2)) >= ((1 * ($1 . I1)) + 0 );

        

         A5: { p where p be n9 -element XFinSequence of NAT : P3[p] } is diophantine Subset of (n9 -xtuples_of NAT ) by Th8;

        defpred P4[ XFinSequence of NAT ] means (1 * ($1 . N3)) > ((1 * ($1 . I1)) + 0 );

        

         A6: { p where p be n9 -element XFinSequence of NAT : P4[p] } is diophantine Subset of (n9 -xtuples_of NAT ) by Th7;

        defpred P5[ XFinSequence of NAT ] means (1 * ($1 . I1)) >= ((1 * ($1 . I3)) + 0 );

        

         A7: { p where p be n9 -element XFinSequence of NAT : P5[p] } is diophantine Subset of (n9 -xtuples_of NAT ) by Th8;

        defpred P6[ XFinSequence of NAT ] means [(1 * ($1 . N4)), (1 * ($1 . N5))] is Pell's_solution of (((1 * ($1 . N3)) ^2 ) -' 1);

        

         A8: { p where p be n9 -element XFinSequence of NAT : P6[p] } is diophantine Subset of (n9 -xtuples_of NAT ) by Th22;

        defpred P7[ XFinSequence of NAT ] means ((1 * ($1 . N5)),(1 * ($1 . I1))) are_congruent_mod (1 * ($1 . N1));

        

         A9: { p where p be n9 -element XFinSequence of NAT : P7[p] } is diophantine Subset of (n9 -xtuples_of NAT ) by Th21;

        defpred PA[ XFinSequence of NAT ] means ((1 * ($1 . N3)),(1 * ($1 . I2))) are_congruent_mod (1 * ($1 . N1));

        

         A10: { p where p be n9 -element XFinSequence of NAT : PA[p] } is diophantine Subset of (n9 -xtuples_of NAT ) by Th21;

        defpred PB[ XFinSequence of NAT ] means ((1 * ($1 . N5)),(1 * ($1 . I3))) are_congruent_mod (1 * ($1 . N6));

        

         A11: { p where p be n9 -element XFinSequence of NAT : PB[p] } is diophantine Subset of (n9 -xtuples_of NAT ) by Th21;

        defpred PC[ XFinSequence of NAT ] means ((1 * ($1 . N3)),(1 * ($1 . N8))) are_congruent_mod (1 * ($1 . N6));

        

         A12: { p where p be n9 -element XFinSequence of NAT : PC[p] } is diophantine Subset of (n9 -xtuples_of NAT ) by Th21;

        defpred PD[ XFinSequence of NAT ] means ((1 * ($1 . N2)),( 0 * ($1 . N3))) are_congruent_mod (1 * ($1 . N7));

        

         A13: { p where p be n9 -element XFinSequence of NAT : PD[p] } is diophantine Subset of (n9 -xtuples_of NAT ) by Th21;

        defpred PE[ XFinSequence of NAT ] means 1 = ($1 . N8);

        

         A14: { p where p be n9 -element XFinSequence of NAT : PE[p] } is diophantine Subset of (n9 -xtuples_of NAT ) by Th14;

        defpred PF[ XFinSequence of NAT ] means (2 * ($1 . I1)) = ($1 . N6);

        

         A15: { p where p be n9 -element XFinSequence of NAT : PF[p] } is diophantine Subset of (n9 -xtuples_of NAT ) by Th12;

        defpred PG[ XFinSequence of NAT ] means ((1 * ($1 . I1)) * ($1 . I1)) = (1 * ($1 . N7));

        

         A16: { p where p be n9 -element XFinSequence of NAT : PG[p] } is diophantine Subset of (n9 -xtuples_of NAT ) by Th9;

        defpred P01[ XFinSequence of NAT ] means P0[$1] & P1[$1];

        defpred P23[ XFinSequence of NAT ] means P2[$1] & P3[$1];

        defpred P45[ XFinSequence of NAT ] means P4[$1] & P5[$1];

        defpred P67[ XFinSequence of NAT ] means P6[$1] & P7[$1];

        defpred PAB[ XFinSequence of NAT ] means PA[$1] & PB[$1];

        defpred PCD[ XFinSequence of NAT ] means PC[$1] & PD[$1];

        defpred PEF[ XFinSequence of NAT ] means PE[$1] & PF[$1];

        { p where p be n9 -element XFinSequence of NAT : P0[p] & P1[p] } is diophantine Subset of (n9 -xtuples_of NAT ) from IntersectionDiophantine( A2, A3);

        then

         A17: { p where p be n9 -element XFinSequence of NAT : P01[p] } is diophantine Subset of (n9 -xtuples_of NAT );

        { p where p be n9 -element XFinSequence of NAT : P2[p] & P3[p] } is diophantine Subset of (n9 -xtuples_of NAT ) from IntersectionDiophantine( A4, A5);

        then

         A18: { p where p be n9 -element XFinSequence of NAT : P23[p] } is diophantine Subset of (n9 -xtuples_of NAT );

        { p where p be n9 -element XFinSequence of NAT : P4[p] & P5[p] } is diophantine Subset of (n9 -xtuples_of NAT ) from IntersectionDiophantine( A6, A7);

        then

         A19: { p where p be n9 -element XFinSequence of NAT : P45[p] } is diophantine Subset of (n9 -xtuples_of NAT );

        { p where p be n9 -element XFinSequence of NAT : P6[p] & P7[p] } is diophantine Subset of (n9 -xtuples_of NAT ) from IntersectionDiophantine( A8, A9);

        then

         A20: { p where p be n9 -element XFinSequence of NAT : P67[p] } is diophantine Subset of (n9 -xtuples_of NAT );

        { p where p be n9 -element XFinSequence of NAT : PA[p] & PB[p] } is diophantine Subset of (n9 -xtuples_of NAT ) from IntersectionDiophantine( A10, A11);

        then

         A21: { p where p be n9 -element XFinSequence of NAT : PAB[p] } is diophantine Subset of (n9 -xtuples_of NAT );

        { p where p be n9 -element XFinSequence of NAT : PC[p] & PD[p] } is diophantine Subset of (n9 -xtuples_of NAT ) from IntersectionDiophantine( A12, A13);

        then

         A22: { p where p be n9 -element XFinSequence of NAT : PCD[p] } is diophantine Subset of (n9 -xtuples_of NAT );

        { p where p be n9 -element XFinSequence of NAT : PE[p] & PF[p] } is diophantine Subset of (n9 -xtuples_of NAT ) from IntersectionDiophantine( A14, A15);

        then

         A23: { p where p be n9 -element XFinSequence of NAT : PEF[p] } is diophantine Subset of (n9 -xtuples_of NAT );

        defpred P0123[ XFinSequence of NAT ] means P01[$1] & P23[$1];

        defpred P4567[ XFinSequence of NAT ] means P45[$1] & P67[$1];

        defpred PABCD[ XFinSequence of NAT ] means PAB[$1] & PCD[$1];

        defpred PEFG[ XFinSequence of NAT ] means PEF[$1] & PG[$1];

        { p where p be n9 -element XFinSequence of NAT : P01[p] & P23[p] } is diophantine Subset of (n9 -xtuples_of NAT ) from IntersectionDiophantine( A17, A18);

        then

         A24: { p where p be n9 -element XFinSequence of NAT : P0123[p] } is diophantine Subset of (n9 -xtuples_of NAT );

        { p where p be n9 -element XFinSequence of NAT : P45[p] & P67[p] } is diophantine Subset of (n9 -xtuples_of NAT ) from IntersectionDiophantine( A19, A20);

        then

         A25: { p where p be n9 -element XFinSequence of NAT : P4567[p] } is diophantine Subset of (n9 -xtuples_of NAT );

        { p where p be n9 -element XFinSequence of NAT : PAB[p] & PCD[p] } is diophantine Subset of (n9 -xtuples_of NAT ) from IntersectionDiophantine( A21, A22);

        then

         A26: { p where p be n9 -element XFinSequence of NAT : PABCD[p] } is diophantine Subset of (n9 -xtuples_of NAT );

        { p where p be n9 -element XFinSequence of NAT : PEF[p] & PG[p] } is diophantine Subset of (n9 -xtuples_of NAT ) from IntersectionDiophantine( A23, A16);

        then

         A27: { p where p be n9 -element XFinSequence of NAT : PEFG[p] } is diophantine Subset of (n9 -xtuples_of NAT );

        defpred P01234567[ XFinSequence of NAT ] means P0123[$1] & P4567[$1];

        defpred PABCDEFG[ XFinSequence of NAT ] means PABCD[$1] & PEFG[$1];

        { p where p be n9 -element XFinSequence of NAT : P0123[p] & P4567[p] } is diophantine Subset of (n9 -xtuples_of NAT ) from IntersectionDiophantine( A24, A25);

        then

         A28: { p where p be n9 -element XFinSequence of NAT : P01234567[p] } is diophantine Subset of (n9 -xtuples_of NAT );

        { p where p be n9 -element XFinSequence of NAT : PABCD[p] & PEFG[p] } is diophantine Subset of (n9 -xtuples_of NAT ) from IntersectionDiophantine( A26, A27);

        then

         A29: { p where p be n9 -element XFinSequence of NAT : PABCDEFG[p] } is diophantine Subset of (n9 -xtuples_of NAT );

        defpred P01234567ABCDEFG[ XFinSequence of NAT ] means P01234567[$1] & PABCDEFG[$1];

        

         A30: { p where p be n9 -element XFinSequence of NAT : P01234567[p] & PABCDEFG[p] } is diophantine Subset of (n9 -xtuples_of NAT ) from IntersectionDiophantine( A28, A29);

        set DD = { p where p be n9 -element XFinSequence of NAT : P01234567ABCDEFG[p] };

        set DDR = { (p | n) where p be n9 -element XFinSequence of NAT : p in DD };

        

         A31: DDR is diophantine Subset of (n -xtuples_of NAT ) by Th5, A30, NAT_1: 11;

        

         A32: DDR c= WW

        proof

          let o be object such that

           A33: o in DDR;

          consider p be n9 -element XFinSequence of NAT such that

           A34: o = (p | n) & p in DD by A33;

          consider q be n9 -element XFinSequence of NAT such that

           A35: p = q & P01234567ABCDEFG[q] by A34;

          ( len p) = n9 & n9 >= n by CARD_1:def 7, NAT_1: 11;

          then ( len (p | n)) = n by AFINSQ_1: 54;

          then

          reconsider pn = (p | n) as n -element XFinSequence of NAT by CARD_1:def 7;

          

           A36: (pn . I3) = (p . i3) & (pn . I2) = (p . i2) & ((p | n) . I1) = (p . i1) by A1, Th4;

          (1 * (p . I2)) > (( 0 * (p . I1)) + 1) & [(1 * (p . N)), (1 * (p . I1))] is Pell's_solution of (((1 * (p . I2)) ^2 ) -' 1) & [(1 * (p . N1)), (1 * (p . N2))] is Pell's_solution of (((1 * (p . I2)) ^2 ) -' 1) & (1 * (p . N2)) >= ((1 * (p . I1)) + 0 ) & (1 * (p . N3)) > ((1 * (p . I1)) + 0 ) & (1 * (p . I1)) >= ((1 * (p . I3)) + 0 ) & [(1 * (p . N4)), (1 * (p . N5))] is Pell's_solution of (((1 * (p . N3)) ^2 ) -' 1) & ((1 * (p . N5)),(1 * (p . I1))) are_congruent_mod (1 * (p . N1)) & ((1 * (p . N3)),(1 * (p . I2))) are_congruent_mod (1 * (p . N1)) & ((1 * (p . N5)),(1 * (p . I3))) are_congruent_mod (1 * (2 * (p . I1))) & ((1 * (p . N3)),(1 * 1)) are_congruent_mod (1 * (2 * (p . I1))) & ((1 * (p . N2)),( 0 * (p . N3))) are_congruent_mod ((p . I1) ^2 ) by SQUARE_1:def 1, A35;

          then (pn . i1) = ( Py ((pn . i2),(pn . i3))) & (pn . i2) > 1 by HILB10_1: 38, A36;

          hence thesis by A34;

        end;

        WW c= DDR

        proof

          let o be object such that

           A37: o in WW;

          consider p such that

           A38: o = p & (p . i1) = ( Py ((p . i2),(p . i3))) & (p . i2) > 1 by A37;

          set y = (p . i1), a = (p . i2), z = (p . i3);

          consider x,x1,y1,A,x2,y2 be Nat such that

           A39: 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 ) by A38, HILB10_1: 38;

          reconsider x, x1, y1, A, x2, y2 as Element of NAT by ORDINAL1:def 12;

          reconsider 2y = (2 * y) as Element of NAT ;

          reconsider yy = (y * y) as Element of NAT ;

          reconsider Z = 1 as Element of NAT ;

          set Y = (((((((( <%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>);

          set PY = (p ^ Y);

          

           A40: ( len p) = n & ( len Y) = 9 by CARD_1:def 7;

          

           A41: (PY | n) = p by A40, AFINSQ_1: 57;

           0 in ( dom Y) by A40, AFINSQ_1: 66;

          

          then

           A42: (PY . (n + 0 )) = (Y . 0 ) by A40, AFINSQ_1:def 3

          .= x by AFINSQ_1: 50;

          1 in ( dom Y) by A40, AFINSQ_1: 66;

          

          then

           A43: (PY . (n + 1)) = (Y . 1) by A40, AFINSQ_1:def 3

          .= x1 by AFINSQ_1: 50;

          2 in ( dom Y) by A40, AFINSQ_1: 66;

          

          then

           A44: (PY . (n + 2)) = (Y . 2) by A40, AFINSQ_1:def 3

          .= y1 by AFINSQ_1: 50;

          3 in ( dom Y) by A40, AFINSQ_1: 66;

          

          then

           A45: (PY . (n + 3)) = (Y . 3) by A40, AFINSQ_1:def 3

          .= A by AFINSQ_1: 50;

          4 in ( dom Y) by A40, AFINSQ_1: 66;

          

          then

           A46: (PY . (n + 4)) = (Y . 4) by A40, AFINSQ_1:def 3

          .= x2 by AFINSQ_1: 50;

          5 in ( dom Y) by A40, AFINSQ_1: 66;

          

          then

           A47: (PY . (n + 5)) = (Y . 5) by A40, AFINSQ_1:def 3

          .= y2 by AFINSQ_1: 50;

          6 in ( dom Y) by A40, AFINSQ_1: 66;

          

          then (PY . (n + 6)) = (Y . 6) by A40, AFINSQ_1:def 3

          .= 2y by AFINSQ_1: 50;

          then

           A48: (PY . N6) = (2 * y) = (2 * (PY . I1)) by A41, A1, Th4;

          7 in ( dom Y) by A40, AFINSQ_1: 66;

          

          then

           A49: (PY . (n + 7)) = (Y . 7) by A40, AFINSQ_1:def 3

          .= yy by AFINSQ_1: 50;

          8 in ( dom Y) by A40, AFINSQ_1: 66;

          

          then

           A50: (PY . (n + 8)) = (Y . 8) by A40, AFINSQ_1:def 3

          .= Z by AFINSQ_1: 50;

           P01234567ABCDEFG[PY] by SQUARE_1:def 1, A39, A42, A45, A46, A47, A1, Th4, A43, A41, A50, A48, A49, A44;

          then PY in DD;

          hence thesis by A38, A41;

        end;

        hence thesis by A31, A32, XBOOLE_0:def 10;

      end;

    end;

    theorem :: HILB10_3:24

    for i1, i2, i3 holds { p : (p . i2) = ((p . i1) |^ (p . i3)) } is diophantine Subset of (n -xtuples_of NAT )

    proof

      let i1, i2, i3;

      set n7 = (n + 7);

      set WW = { p : (p . i2) = ((p . i1) |^ (p . i3)) };

      WW c= (n -xtuples_of NAT )

      proof

        let y be object;

        assume y in WW;

        then ex p st y = p & (p . i2) = ((p . i1) |^ (p . i3));

        hence thesis by HILB10_2:def 5;

      end;

      then

      reconsider WW as Subset of (n -xtuples_of NAT );

      per cases ;

        suppose n = 0 ;

        then WW is diophantine Subset of (n -xtuples_of NAT );

        hence thesis;

      end;

        suppose

         A1: n <> 0 ;

        n = (n + 0 );

        then

        reconsider N = n, I1 = i1, I2 = i2, I3 = i3, N1 = (n + 1), N2 = (n + 2), N3 = (n + 3), N4 = (n + 4), N5 = (n + 5), N6 = (n + 6) as Element of n7 by Th2, Th3;

        defpred P0[ XFinSequence of NAT ] means ($1 . I1) = 0 ;

        

         A2: { p where p be n7 -element XFinSequence of NAT : P0[p] } is diophantine Subset of (n7 -xtuples_of NAT ) by Th14;

        defpred P1[ XFinSequence of NAT ] means ($1 . I1) = 1;

        

         A3: { p where p be n7 -element XFinSequence of NAT : P1[p] } is diophantine Subset of (n7 -xtuples_of NAT ) by Th14;

        defpred P2[ XFinSequence of NAT ] means (1 * ($1 . I1)) > (( 0 * ($1 . I2)) + 1);

        

         A4: { p where p be n7 -element XFinSequence of NAT : P2[p] } is diophantine Subset of (n7 -xtuples_of NAT ) by Th7;

        defpred P3[ XFinSequence of NAT ] means ($1 . I2) = 0 ;

        

         A5: { p where p be n7 -element XFinSequence of NAT : P3[p] } is diophantine Subset of (n7 -xtuples_of NAT ) by Th14;

        defpred P4[ XFinSequence of NAT ] means ($1 . I2) = 1;

        

         A6: { p where p be n7 -element XFinSequence of NAT : P4[p] } is diophantine Subset of (n7 -xtuples_of NAT ) by Th14;

        defpred P5[ XFinSequence of NAT ] means ($1 . I3) = 0 ;

        

         A7: { p where p be n7 -element XFinSequence of NAT : P5[p] } is diophantine Subset of (n7 -xtuples_of NAT ) by Th14;

        defpred P6[ XFinSequence of NAT ] means (1 * ($1 . I3)) > (( 0 * ($1 . I1)) + 0 );

        

         A8: { p where p be n7 -element XFinSequence of NAT : P6[p] } is diophantine Subset of (n7 -xtuples_of NAT ) by Th7;

        defpred PA[ XFinSequence of NAT ] means (1 * ($1 . N4)) = ((1 * ($1 . I3)) + 1);

        

         A9: { p where p be n7 -element XFinSequence of NAT : PA[p] } is diophantine Subset of (n7 -xtuples_of NAT ) by Th6;

        defpred PB[ XFinSequence of NAT ] means (1 * ($1 . N5)) = ((1 * ($1 . N3)) * ($1 . I1));

        

         A10: { p where p be n7 -element XFinSequence of NAT : PB[p] } is diophantine Subset of (n7 -xtuples_of NAT ) by Th9;

        defpred PC[ XFinSequence of NAT ] means ($1 . N) = ( Py (($1 . I1),($1 . N4))) & ($1 . I1) > 1;

        

         A11: { p where p be n7 -element XFinSequence of NAT : PC[p] } is diophantine Subset of (n7 -xtuples_of NAT ) by Th23;

        defpred PD[ XFinSequence of NAT ] means (1 * ($1 . N3)) > ((2 * ($1 . I3)) * ($1 . N));

        

         A12: { p where p be n7 -element XFinSequence of NAT : PD[p] } is diophantine Subset of (n7 -xtuples_of NAT ) by Th17;

        defpred PE[ XFinSequence of NAT ] means ($1 . N1) = ( Py (($1 . N3),($1 . N4))) & ($1 . N3) > 1;

        

         A13: { p where p be n7 -element XFinSequence of NAT : PE[p] } is diophantine Subset of (n7 -xtuples_of NAT ) by Th23;

        defpred PF[ XFinSequence of NAT ] means ($1 . N2) = ( Py (($1 . N5),($1 . N4))) & ($1 . N5) > 1;

        

         A14: { p where p be n7 -element XFinSequence of NAT : PF[p] } is diophantine Subset of (n7 -xtuples_of NAT ) by Th23;

        defpred PG[ XFinSequence of NAT ] means (1 * ($1 . N6)) = ((1 * ($1 . I2)) * ($1 . N1));

        

         A15: { p where p be n7 -element XFinSequence of NAT : PG[p] } is diophantine Subset of (n7 -xtuples_of NAT ) by Th9;

        defpred PH[ XFinSequence of NAT ] means (1 * ($1 . N6)) >= ((1 * ($1 . N2)) + 0 );

        

         A16: { p where p be n7 -element XFinSequence of NAT : PH[p] } is diophantine Subset of (n7 -xtuples_of NAT ) by Th8;

        defpred PI[ XFinSequence of NAT ] means (2 * ($1 . N6)) < ((1 * ($1 . N1)) + (2 * ($1 . N2)));

        

         A17: { p where p be n7 -element XFinSequence of NAT : PI[p] } is diophantine Subset of (n7 -xtuples_of NAT ) by Th18;

        defpred PJ[ XFinSequence of NAT ] means (1 * ($1 . N2)) >= ((1 * ($1 . N6)) + 0 );

        

         A18: { p where p be n7 -element XFinSequence of NAT : PJ[p] } is diophantine Subset of (n7 -xtuples_of NAT ) by Th8;

        defpred PK[ XFinSequence of NAT ] means (( - 2) * ($1 . N6)) < ((1 * ($1 . N1)) + (( - 2) * ($1 . N2)));

        

         A19: { p where p be n7 -element XFinSequence of NAT : PK[p] } is diophantine Subset of (n7 -xtuples_of NAT ) by Th18;

        defpred P45[ XFinSequence of NAT ] means P4[$1] & P5[$1];

        defpred P03[ XFinSequence of NAT ] means P0[$1] & P3[$1];

        defpred P036[ XFinSequence of NAT ] means P03[$1] & P6[$1];

        defpred P14[ XFinSequence of NAT ] means P1[$1] & P4[$1];

        defpred P146[ XFinSequence of NAT ] means P14[$1] & P6[$1];

        defpred P26[ XFinSequence of NAT ] means P2[$1] & P6[$1];

        defpred PHI[ XFinSequence of NAT ] means PH[$1] & PI[$1];

        defpred PJK[ XFinSequence of NAT ] means PJ[$1] & PK[$1];

        { p where p be n7 -element XFinSequence of NAT : P4[p] & P5[p] } is diophantine Subset of (n7 -xtuples_of NAT ) from IntersectionDiophantine( A6, A7);

        then

         A20: { p where p be n7 -element XFinSequence of NAT : P45[p] } is diophantine Subset of (n7 -xtuples_of NAT );

        { p where p be n7 -element XFinSequence of NAT : P0[p] & P3[p] } is diophantine Subset of (n7 -xtuples_of NAT ) from IntersectionDiophantine( A2, A5);

        then

         A21: { p where p be n7 -element XFinSequence of NAT : P03[p] } is diophantine Subset of (n7 -xtuples_of NAT );

        { p where p be n7 -element XFinSequence of NAT : P03[p] & P6[p] } is diophantine Subset of (n7 -xtuples_of NAT ) from IntersectionDiophantine( A21, A8);

        then

         A22: { p where p be n7 -element XFinSequence of NAT : P036[p] } is diophantine Subset of (n7 -xtuples_of NAT );

        { p where p be n7 -element XFinSequence of NAT : P1[p] & P4[p] } is diophantine Subset of (n7 -xtuples_of NAT ) from IntersectionDiophantine( A3, A6);

        then

         A23: { p where p be n7 -element XFinSequence of NAT : P14[p] } is diophantine Subset of (n7 -xtuples_of NAT );

        { p where p be n7 -element XFinSequence of NAT : P14[p] & P6[p] } is diophantine Subset of (n7 -xtuples_of NAT ) from IntersectionDiophantine( A23, A8);

        then

         A24: { p where p be n7 -element XFinSequence of NAT : P146[p] } is diophantine Subset of (n7 -xtuples_of NAT );

        { p where p be n7 -element XFinSequence of NAT : P2[p] & P6[p] } is diophantine Subset of (n7 -xtuples_of NAT ) from IntersectionDiophantine( A4, A8);

        then

         A25: { p where p be n7 -element XFinSequence of NAT : P26[p] } is diophantine Subset of (n7 -xtuples_of NAT );

        { p where p be n7 -element XFinSequence of NAT : PH[p] & PI[p] } is diophantine Subset of (n7 -xtuples_of NAT ) from IntersectionDiophantine( A16, A17);

        then

         A26: { p where p be n7 -element XFinSequence of NAT : PHI[p] } is diophantine Subset of (n7 -xtuples_of NAT );

        { p where p be n7 -element XFinSequence of NAT : PJ[p] & PK[p] } is diophantine Subset of (n7 -xtuples_of NAT ) from IntersectionDiophantine( A18, A19);

        then

         A27: { p where p be n7 -element XFinSequence of NAT : PJK[p] } is diophantine Subset of (n7 -xtuples_of NAT );

        defpred PHIJK[ XFinSequence of NAT ] means PHI[$1] or PJK[$1];

        { p where p be n7 -element XFinSequence of NAT : PHI[p] or PJK[p] } is diophantine Subset of (n7 -xtuples_of NAT ) from UnionDiophantine( A26, A27);

        then

         A28: { p where p be n7 -element XFinSequence of NAT : PHIJK[p] } is diophantine Subset of (n7 -xtuples_of NAT );

        defpred P45036[ XFinSequence of NAT ] means P45[$1] or P036[$1];

        { p where p be n7 -element XFinSequence of NAT : P45[p] or P036[p] } is diophantine Subset of (n7 -xtuples_of NAT ) from UnionDiophantine( A20, A22);

        then

         A29: { p where p be n7 -element XFinSequence of NAT : P45036[p] } is diophantine Subset of (n7 -xtuples_of NAT );

        defpred P45036146[ XFinSequence of NAT ] means P45036[$1] or P146[$1];

        { p where p be n7 -element XFinSequence of NAT : P45036[p] or P146[p] } is diophantine Subset of (n7 -xtuples_of NAT ) from UnionDiophantine( A29, A24);

        then

         A30: { p where p be n7 -element XFinSequence of NAT : P45036146[p] } is diophantine Subset of (n7 -xtuples_of NAT );

        defpred PAB[ XFinSequence of NAT ] means PA[$1] & PB[$1];

        defpred PCD[ XFinSequence of NAT ] means PC[$1] & PD[$1];

        defpred PCDE[ XFinSequence of NAT ] means PCD[$1] & PE[$1];

        defpred PCDEF[ XFinSequence of NAT ] means PCDE[$1] & PF[$1];

        defpred PCDEFHIJK[ XFinSequence of NAT ] means PCDEF[$1] & PHIJK[$1];

        defpred P26CDEFHIJK[ XFinSequence of NAT ] means P26[$1] & PCDEFHIJK[$1];

        defpred P26CDEFHIJKAB[ XFinSequence of NAT ] means P26CDEFHIJK[$1] & PAB[$1];

        defpred P26CDEFHIJKABG[ XFinSequence of NAT ] means P26CDEFHIJKAB[$1] & PG[$1];

        { p where p be n7 -element XFinSequence of NAT : PA[p] & PB[p] } is diophantine Subset of (n7 -xtuples_of NAT ) from IntersectionDiophantine( A9, A10);

        then

         A31: { p where p be n7 -element XFinSequence of NAT : PAB[p] } is diophantine Subset of (n7 -xtuples_of NAT );

        { p where p be n7 -element XFinSequence of NAT : PC[p] & PD[p] } is diophantine Subset of (n7 -xtuples_of NAT ) from IntersectionDiophantine( A11, A12);

        then

         A32: { p where p be n7 -element XFinSequence of NAT : PCD[p] } is diophantine Subset of (n7 -xtuples_of NAT );

        { p where p be n7 -element XFinSequence of NAT : PCD[p] & PE[p] } is diophantine Subset of (n7 -xtuples_of NAT ) from IntersectionDiophantine( A32, A13);

        then

         A33: { p where p be n7 -element XFinSequence of NAT : PCDE[p] } is diophantine Subset of (n7 -xtuples_of NAT );

        { p where p be n7 -element XFinSequence of NAT : PCDE[p] & PF[p] } is diophantine Subset of (n7 -xtuples_of NAT ) from IntersectionDiophantine( A33, A14);

        then

         A34: { p where p be n7 -element XFinSequence of NAT : PCDEF[p] } is diophantine Subset of (n7 -xtuples_of NAT );

        { p where p be n7 -element XFinSequence of NAT : PCDEF[p] & PHIJK[p] } is diophantine Subset of (n7 -xtuples_of NAT ) from IntersectionDiophantine( A34, A28);

        then

         A35: { p where p be n7 -element XFinSequence of NAT : PCDEFHIJK[p] } is diophantine Subset of (n7 -xtuples_of NAT );

        { p where p be n7 -element XFinSequence of NAT : P26[p] & PCDEFHIJK[p] } is diophantine Subset of (n7 -xtuples_of NAT ) from IntersectionDiophantine( A25, A35);

        then

         A36: { p where p be n7 -element XFinSequence of NAT : P26CDEFHIJK[p] } is diophantine Subset of (n7 -xtuples_of NAT );

        { p where p be n7 -element XFinSequence of NAT : P26CDEFHIJK[p] & PAB[p] } is diophantine Subset of (n7 -xtuples_of NAT ) from IntersectionDiophantine( A36, A31);

        then

         A37: { p where p be n7 -element XFinSequence of NAT : P26CDEFHIJKAB[p] } is diophantine Subset of (n7 -xtuples_of NAT );

        { p where p be n7 -element XFinSequence of NAT : P26CDEFHIJKAB[p] & PG[p] } is diophantine Subset of (n7 -xtuples_of NAT ) from IntersectionDiophantine( A37, A15);

        then

         A38: { p where p be n7 -element XFinSequence of NAT : P26CDEFHIJKABG[p] } is diophantine Subset of (n7 -xtuples_of NAT );

        defpred P4503614626CDEFHIJKABG[ XFinSequence of NAT ] means P45036146[$1] or P26CDEFHIJKABG[$1];

        

         A39: { p where p be n7 -element XFinSequence of NAT : P45036146[p] or P26CDEFHIJKABG[p] } is diophantine Subset of (n7 -xtuples_of NAT ) from UnionDiophantine( A30, A38);

        set DD = { p where p be n7 -element XFinSequence of NAT : P4503614626CDEFHIJKABG[p] };

        set DDR = { (p | n) where p be n7 -element XFinSequence of NAT : p in DD };

        

         A40: DDR is diophantine Subset of (n -xtuples_of NAT ) by Th5, A39, NAT_1: 11;

        

         A41: DDR c= WW

        proof

          let o be object such that

           A42: o in DDR;

          consider p be n7 -element XFinSequence of NAT such that

           A43: o = (p | n) & p in DD by A42;

          consider q be n7 -element XFinSequence of NAT such that

           A44: p = q & P4503614626CDEFHIJKABG[q] by A43;

          ( len p) = n7 & n7 >= n by CARD_1:def 7, NAT_1: 11;

          then ( len (p | n)) = n by AFINSQ_1: 54;

          then

          reconsider pn = (p | n) as n -element XFinSequence of NAT by CARD_1:def 7;

          set x = (pn . i1), y = (pn . i2), z = (pn . i3);

          set y1 = (p . N), y2 = (p . N1), y3 = (p . N2), K = (p . N3);

          

           A45: x = (p . i1) & y = (p . i2) & z = (p . i3) by A1, Th4;

          (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

            per cases by A44, A45;

              suppose y = 1 & z = 0 ;

              hence thesis;

            end;

              suppose x = 0 & y = 0 & z > 0 ;

              hence thesis;

            end;

              suppose x = 1 & y = 1 & z > 0 ;

              hence thesis;

            end;

              suppose

               A46: (((1 * x) > (( 0 * y) + 1)) & ((1 * z) > (( 0 * x) + 0 )) & (y1 = ( Py (x,(z + 1)))) & ((1 * K) > ((2 * z) * y1)) & (y2 = ( Py (K,(z + 1)))) & ((1 * y3) = ( Py ((K * x),(z + 1)))) & (((((1 * y) * y2) >= ((1 * y3) + 0 )) & (((2 * y) * y2) < ((1 * y2) + (2 * y3)))) or (((1 * y3) >= (y * y2)) & (((( - 2) * y) * y2) < ((1 * y2) + (( - 2) * y3))))));

              (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

                thus x > 1 & z > 0 by A46;

                take y1, y2, y3, K;

                thus y1 = ( Py (x,(z + 1))) & K > ((2 * z) * y1) & y2 = ( Py (K,(z + 1))) & y3 = ( Py ((K * x),(z + 1))) by A46;

                x is non trivial by A46, NEWTON03:def 1;

                then y1 > 0 & (2 * z) > 0 by A46, XREAL_1: 129, HILB10_1: 13;

                then ((2 * z) * y1) > 0 by XREAL_1: 129;

                then ((2 * z) * y1) >= 1 by NAT_1: 14;

                then K > 1 by A46, XXREAL_0: 2;

                then K is non trivial by NEWTON03:def 1;

                then

                 A47: y2 > 0 by A46, HILB10_1: 13;

                per cases by A46;

                  suppose ((y * y2) >= y3) & (((2 * y) * y2) < ((1 * y2) + (2 * y3)));

                  then (((y * y2) / y2) >= (y3 / y2)) & ((((2 * y) * y2) / y2) < (((1 * y2) + (2 * y3)) / y2)) by A47, XREAL_1: 74, XREAL_1: 72;

                  then (y >= (y3 / y2)) & ((2 * y) < (((1 * y2) + (2 * y3)) / y2)) by XCMPLX_1: 89, A47;

                  then

                   A48: ((y - (y3 / y2)) >= ((y3 / y2) - (y3 / y2))) & (((2 * y) * 1) < (((1 * y2) / y2) + ((2 * y3) / y2))) by XREAL_1: 9, XCMPLX_1: 62;

                  then ((y - (y3 / y2)) >= 0 ) & ((2 * y) < (1 + ((2 * y3) / y2))) by XCMPLX_1: 89, A47;

                  then (((2 * y) / 2) < ((1 + ((2 * y3) / y2)) / 2)) by XREAL_1: 74;

                  then ((y / (2 / 2)) < ((1 / 2) + (((2 * y3) / y2) / 2)));

                  then

                   A49: y < ((1 / 2) + ((2 * y3) / (y2 * 2))) by XCMPLX_1: 78;

                  ((2 * y3) / (y2 * 2)) = (y3 / y2) by XCMPLX_1: 91;

                  then ((y - (y3 / y2)) < (((1 / 2) + (y3 / y2)) - (y3 / y2))) by A49, XREAL_1: 9;

                  hence thesis by A48;

                end;

                  suppose

                   A50: (y3 >= (y * y2)) & (((( - 2) * y) * y2) < ((1 * y2) + (( - 2) * y3)));

                  then ((y3 / y2) >= ((y * y2) / y2)) & (((( - 2) * y) * y2) < ((1 * y2) + (( - 2) * y3))) by XREAL_1: 72;

                  then ((y3 / y2) >= y) by A47, XCMPLX_1: 89;

                  then

                   A51: (((y3 / y2) - y) >= (y - y)) by XREAL_1: 9;

                  ((((( - 2) * y) * y2) / y2) < (((1 * y2) + (( - 2) * y3)) / y2)) by A47, A50, XREAL_1: 74;

                  then ((( - 2) * y) < (((1 * y2) + (( - 2) * y3)) / y2)) by A47, XCMPLX_1: 89;

                  then ((( - 2) * y) < (((1 * y2) / y2) + ((( - 2) * y3) / y2))) by XCMPLX_1: 62;

                  then ((( - 2) * y) < (1 + ((( - 2) * y3) / y2))) by A47, XCMPLX_1: 89;

                  then

                   A52: (((1 + ((( - 2) * y3) / y2)) / ( - 2)) < ((( - 2) * y) / ( - 2))) by XREAL_1: 75;

                  

                   A53: (((( - 2) * y3) / y2) / ( - 2)) = ((( - 2) * y3) / (y2 * ( - 2))) by XCMPLX_1: 78

                  .= (y3 / y2) by XCMPLX_1: 91;

                  (( - (1 / 2)) + (y3 / y2)) < y by A52, A53;

                  then (1 / 2) > ( - (y - (y3 / y2))) by XREAL_1: 25, XREAL_1: 20;

                  hence thesis by A51;

                end;

              end;

              hence thesis;

            end;

          end;

          then (pn . i2) = ((pn . i1) |^ (pn . i3)) by HILB10_1: 39;

          hence thesis by A43;

        end;

        WW c= DDR

        proof

          let o be object such that

           A54: o in WW;

          consider p such that

           A55: o = p & (p . i2) = ((p . i1) |^ (p . i3)) by A54;

          set x = (p . i1), y = (p . i2), z = (p . i3);

          per cases by A55, HILB10_1: 39;

            suppose

             A56: (y = 1 & z = 0 ) or (x = 0 & y = 0 & z > 0 ) or (x = 1 & y = 1 & z > 0 );

            reconsider Z = 0 , z1 = (z + 1) as Element of NAT ;

            set Y = (((((( <%Z%> ^ <%Z%>) ^ <%Z%>) ^ <%Z%>) ^ <%z1%>) ^ <%Z%>) ^ <%Z%>);

            set PY = (p ^ Y);

            

             A57: ( len p) = n & ( len Y) = 7 by CARD_1:def 7;

            

             A58: (PY | n) = p by A57, AFINSQ_1: 57;

             P45[PY] or P036[PY] or P146[PY] by A56, A58, A1, Th4;

            then PY in DD;

            hence thesis by A55, A58;

          end;

            suppose

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

            then

            consider y1,y2,y3,K be Nat such that

             A60: 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 y1, y2, y3, K, z1 = (z + 1) as Element of NAT by ORDINAL1:def 12;

            reconsider Kx = (K * x), yy2 = (y * y2) as Element of NAT ;

            set Y = (((((( <%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>);

            set PY = (p ^ Y);

            

             A61: ( len p) = n & ( len Y) = 7 by CARD_1:def 7;

            

             A62: (PY | n) = p by A61, AFINSQ_1: 57;

            4 in ( dom Y) by A61, AFINSQ_1: 66;

            

            then

             A63: (PY . (n + 4)) = (Y . 4) by A61, AFINSQ_1:def 3

            .= z1 by AFINSQ_1: 48;

             0 in ( dom Y) by A61, AFINSQ_1: 66;

            

            then

             A64: (PY . (n + 0 )) = (Y . 0 ) by A61, AFINSQ_1:def 3

            .= y1 by AFINSQ_1: 48;

            3 in ( dom Y) by A61, AFINSQ_1: 66;

            

            then

             A65: (PY . (n + 3)) = (Y . 3) by A61, AFINSQ_1:def 3

            .= K by AFINSQ_1: 48;

            5 in ( dom Y) by A61, AFINSQ_1: 66;

            

            then

             A66: (PY . (n + 5)) = (Y . 5) by A61, AFINSQ_1:def 3

            .= Kx by AFINSQ_1: 48;

            x is non trivial by A59, NEWTON03:def 1;

            then y1 > 0 & z > 0 by A59, A60, HILB10_1: 13;

            then (z * y1) > 0 by XREAL_1: 129;

            then (2 * (z * y1)) >= (2 * 1) by XREAL_1: 64, NAT_1: 14;

            then

             A67: K >= (1 + 1) by XXREAL_0: 2, A60;

            then

             A68: K > 1 by XXREAL_0: 2;

            1 in ( dom Y) by A61, AFINSQ_1: 66;

            

            then

             A69: (PY . (n + 1)) = (Y . 1) by A61, AFINSQ_1:def 3

            .= y2 by AFINSQ_1: 48;

            

             A70: (K * x) > (1 * 1) by A68, A59, XREAL_1: 97;

            2 in ( dom Y) by A61, AFINSQ_1: 66;

            

            then

             A71: (PY . (n + 2)) = (Y . 2) by A61, AFINSQ_1:def 3

            .= y3 by AFINSQ_1: 48;

            6 in ( dom Y) by A61, AFINSQ_1: 66;

            

            then

             A72: (PY . (n + 6)) = (Y . 6) by A61, AFINSQ_1:def 3

            .= yy2 by AFINSQ_1: 48;

            x is non trivial by A59, NEWTON03:def 1;

            then y1 > 0 & (2 * z) > 0 by A60, A59, XREAL_1: 129, HILB10_1: 13;

            then ((2 * z) * y1) > 0 by XREAL_1: 129;

            then ((2 * z) * y1) >= 1 by NAT_1: 14;

            then K > 1 by A60, XXREAL_0: 2;

            then K is non trivial by NEWTON03:def 1;

            then

             A73: y2 > 0 by A60, HILB10_1: 13;

             PHIJK[PY]

            proof

              per cases by A60;

                suppose

                 A74: ((y - (y3 / y2)) >= 0 ) & ((y - (y3 / y2)) < (1 / 2));

                ((y - (y3 / y2)) * y2) >= ( 0 * y2) by A74;

                then ((y * y2) - ((y3 / y2) * y2)) >= 0 ;

                then ((y * y2) - (y3 / (y2 / y2))) >= 0 by XCMPLX_1: 82;

                then ((y * y2) - (y3 / 1)) >= 0 by XCMPLX_1: 60, A73;

                then

                 A75: (((y * y2) - y3) + y3) >= ( 0 + y3) by XREAL_1: 6;

                ((y - (y3 / y2)) * y2) < ((1 / 2) * y2) by A74, XREAL_1: 68, A73;

                then ((y * y2) - ((y3 / y2) * y2)) < ((1 / 2) * y2);

                then ((y * y2) - (y3 / (y2 / y2))) < ((1 / 2) * y2) by XCMPLX_1: 82;

                then ((y * y2) - (y3 / 1)) < ((1 / 2) * y2) by A73, XCMPLX_1: 60;

                then (((y * y2) - y3) * 2) < (((1 / 2) * y2) * 2) by XREAL_1: 68;

                then ((((2 * y) * y2) - (2 * y3)) + (2 * y3)) < ((1 * y2) + (2 * y3)) by XREAL_1: 6;

                hence thesis by A72, A71, A69, A75;

              end;

                suppose

                 A76: (((y3 / y2) - y) >= 0 ) & (((y3 / y2) - y) < (1 / 2));

                then (((y3 / y2) - y) + y) >= ( 0 + y) by XREAL_1: 6;

                then ((y3 / y2) * y2) >= (y * y2) by XREAL_1: 64;

                then (y3 / (y2 / y2)) >= (y * y2) by XCMPLX_1: 82;

                then

                 A77: (y3 / 1) >= (y * y2) by A73, XCMPLX_1: 60;

                (((y3 / y2) - y) * y2) < ((1 / 2) * y2) by A76, XREAL_1: 68, A73;

                then (((y3 / y2) * y2) - (y * y2)) < ((1 / 2) * y2);

                then ((y3 / (y2 / y2)) - (y * y2)) < ((1 / 2) * y2) by XCMPLX_1: 82;

                then ((y3 / 1) - (y * y2)) < ((1 / 2) * y2) by A73, XCMPLX_1: 60;

                then ((y3 - (y * y2)) * 2) < (((1 / 2) * y2) * 2) by XREAL_1: 68;

                then ((( - ((2 * y) * y2)) + (2 * y3)) - (2 * y3)) < ((1 * y2) - (2 * y3)) by XREAL_1: 14;

                hence thesis by A72, A71, A69, A77;

              end;

            end;

            then P26CDEFHIJKABG[PY] by A59, A63, A67, XXREAL_0: 2, A65, A71, A60, A70, A66, A64, A62, A1, Th4, A69, A72;

            then PY in DD;

            hence thesis by A55, A62;

          end;

        end;

        hence thesis by A40, A41, XBOOLE_0:def 10;

      end;

    end;