pells_eq.miz



    begin

    reserve n,n1,n2,k,D for Nat,

r,r1,r2 for Real,

x,y for Integer;

    

     Lm1: 0 < (( [\r/] - r) + 1) <= 1

    proof

      

       A1: (r - r) < (( [\r/] + 1) - r) by INT_1: 29, XREAL_1: 9;

      ( [\r/] - r) <= (r - r) by INT_1:def 6, XREAL_1: 9;

      then (( [\r/] - r) + 1) <= ((r - r) + 1) by XREAL_1: 6;

      hence thesis by A1;

    end;

    

     Lm2: for a,b be Real st a = ( - b) holds |.a.| = |.b.|

    proof

      let a,b be Real such that

       A1: a = ( - b);

      per cases ;

        suppose

         A2: a < 0 ;

        then b > 0 by A1;

        then |.a.| = ( - a) & |.b.| = b by A2, ABSVALUE:def 1;

        hence thesis by A1;

      end;

        suppose a = 0 ;

        hence thesis by A1;

      end;

        suppose

         A3: a > 0 ;

        then b < 0 by A1;

        then |.a.| = a & |.b.| = ( - b) by A3, ABSVALUE:def 1;

        hence thesis by A1;

      end;

    end;

    

     Lm3: r > 0 implies ex n st (1 / n) < r & n > 1

    proof

      assume r > 0 ;

      then

      consider n be Nat such that

       A1: (1 / n) < r & n > 0 by FRECHET: 36;

      n >= 1 by A1, NAT_1: 14;

      then

       A2: (n + n) > (1 + 0 ) by XREAL_1: 8;

      (n + n) > (n + 0 ) by A1, XREAL_1: 8;

      then (1 / (2 * n)) < (1 / n) by A1, XREAL_1: 76;

      then (1 / (2 * n)) < r by A1, XXREAL_0: 2;

      hence thesis by A2;

    end;

    theorem :: PELLS_EQ:1

    

     Th1: for i,j be Integer st j < 0 holds j < (i mod j) <= 0

    proof

      let x,j be Integer;

      assume

       A1: j < 0 ;

      then

       A2: ((x / j) * j) = x by XCMPLX_1: 87;

      ((x / j) - 1) < [\(x / j)/] by INT_1:def 6;

      then ((x / j) - 1) < (x div j) by INT_1:def 9;

      then (((x / j) - 1) * j) > ((x div j) * j) by A1, XREAL_1: 69;

      then (x - j) > (((x div j) * j) - 0 ) by A2;

      then (x - ((x div j) * j)) > (j - 0 ) by XREAL_1: 16;

      hence (x mod j) > j by INT_1:def 10, A1;

       [\(x / j)/] <= (x / j) by INT_1:def 6;

      then (x div j) <= (x / j) by INT_1:def 9;

      then ((x div j) * j) >= ((x / j) * j) by A1, XREAL_1: 65;

      then 0 >= (x - ((x div j) * j)) by A2, XREAL_1: 47;

      hence (x mod j) <= 0 by INT_1:def 10;

    end;

    theorem :: PELLS_EQ:2

    

     Th2: for i,j be Integer st j <> 0 holds |.(i mod j).| < |.j.|

    proof

      let x,j be Integer;

      assume j <> 0 ;

      per cases ;

        suppose j > 0 ;

        then 0 <= (x mod j) < j & |.j.| = j by INT_1: 57, INT_1: 58, ABSVALUE:def 1;

        hence thesis by ABSVALUE:def 1;

      end;

        suppose j < 0 ;

        then

         A2: j < (x mod j) <= 0 & |.j.| = ( - j) by Th1, ABSVALUE:def 1;

        then |.(x mod j).| = ( - (x mod j)) by ABSVALUE: 30;

        hence thesis by A2, XREAL_1: 24;

      end;

    end;

    theorem :: PELLS_EQ:3

    

     Th3: for D be non square Nat holds for a,b,c,d be Integer st (a + (b * ( sqrt D))) = (c + (d * ( sqrt D))) holds a = c & b = d

    proof

      let D be non square Nat;

      let a,b,c,d be Integer such that

       A1: (a + (b * ( sqrt D))) = (c + (d * ( sqrt D)));

      

       A2: (a - c) = ((d - b) * ( sqrt D)) by A1;

      ((a - c) * (a - c)) = (((d - b) * ( sqrt D)) * ((d - b) * ( sqrt D))) by A1

      .= (((d - b) * (d - b)) * (( sqrt D) ^2 ))

      .= (((d - b) * (d - b)) * D) by SQUARE_1:def 2;

      then (d - b) = 0 ;

      then d = b & (a - c) = 0 by A2;

      hence thesis;

    end;

    theorem :: PELLS_EQ:4

    

     Th4: for c,d,n be Nat holds ex a,b be Nat st (a + (b * ( sqrt D))) = ((c + (d * ( sqrt D))) |^ n)

    proof

      let c,d be Nat;

      set cd = (c + (d * ( sqrt D)));

      defpred P[ Nat] means ex a,b be Nat st (a + (b * ( sqrt D))) = (cd |^ $1);

      

       A1: P[ 0 ]

      proof

        take 1, 0 ;

        thus thesis by NEWTON: 4;

      end;

      

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

      proof

        assume P[n];

        then

        consider a,b be Nat such that

         A3: (a + (b * ( sqrt D))) = (cd |^ n);

        

         A4: D = (( sqrt D) ^2 ) by SQUARE_1:def 2;

        (cd |^ (n + 1)) = (cd * (a + (b * ( sqrt D)))) by A3, NEWTON: 6

        .= (((c * a) + ((d * b) * D)) + (( sqrt D) * ((c * b) + (a * d)))) by A4;

        hence thesis;

      end;

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

      hence thesis;

    end;

    theorem :: PELLS_EQ:5

    

     Th5: for c,d be Integer, n be Nat holds ex a,b be Integer st (a + (b * ( sqrt D))) = ((c + (d * ( sqrt D))) |^ n)

    proof

      let c,d be Integer;

      set cd = (c + (d * ( sqrt D)));

      defpred P[ Nat] means ex a,b be Integer st (a + (b * ( sqrt D))) = (cd |^ $1);

      

       A1: P[ 0 ]

      proof

        take 1, 0 ;

        thus thesis by NEWTON: 4;

      end;

      

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

      proof

        assume P[n];

        then

        consider a,b be Integer such that

         A3: (a + (b * ( sqrt D))) = (cd |^ n);

        

         A4: D = (( sqrt D) ^2 ) by SQUARE_1:def 2;

        (cd |^ (n + 1)) = (cd * (a + (b * ( sqrt D)))) by A3, NEWTON: 6

        .= (((c * a) + ((d * b) * D)) + (( sqrt D) * ((c * b) + (a * d)))) by A4;

        hence thesis;

      end;

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

      hence thesis;

    end;

    theorem :: PELLS_EQ:6

    

     Th6: for D be non square Nat holds for a,b,c,d be Integer, n be Nat st (a + (b * ( sqrt D))) = ((c + (d * ( sqrt D))) |^ n) holds (a - (b * ( sqrt D))) = ((c - (d * ( sqrt D))) |^ n)

    proof

      let D be non square Nat;

      set S = ( sqrt D);

      defpred P[ Nat] means for a,b,c,d be Integer st (a + (b * S)) = ((c + (d * S)) |^ $1) holds (a - (b * S)) = ((c - (d * S)) |^ $1);

      

       A1: P[ 0 ]

      proof

        let a,b,c,d be Integer such that

         A2: (a + (b * S)) = ((c + (d * S)) |^ 0 );

        ((c + (d * S)) |^ 0 ) = (1 + ( 0 * S)) = ((c - (d * S)) |^ 0 ) by NEWTON: 4;

        then a = 1 & b = 0 by Th3, A2;

        hence thesis by NEWTON: 4;

      end;

      

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

      proof

        assume

         A4: P[n];

        let a,b,c,d be Integer such that

         A5: (a + (b * S)) = ((c + (d * S)) |^ (n + 1));

        set cPd = (c + (d * S)), cMd = (c - (d * ( sqrt D)));

        consider a1,b1 be Integer such that

         A6: (a1 + (b1 * S)) = (cPd |^ n) by Th5;

        

         A7: D = (S ^2 ) by SQUARE_1:def 2;

        (a + (b * S)) = (cPd * (a1 + (b1 * S))) by A5, A6, NEWTON: 6

        .= (((c * a1) + ((d * b1) * D)) + (S * ((c * b1) + (d * a1)))) by A7;

        then a = ((c * a1) + ((d * b1) * D)) & b = ((c * b1) + (d * a1)) by Th3;

        

        hence (a - (b * S)) = (cMd * (a1 - (b1 * S))) by A7

        .= (cMd * (cMd |^ n)) by A4, A6

        .= (cMd |^ (n + 1)) by NEWTON: 6;

      end;

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

      hence thesis;

    end;

    begin

    theorem :: PELLS_EQ:7

    

     Th7: ex F be FinSequence of NAT st ( len F) = (n + 1) & (for k st k in ( dom F) holds (F . k) = ( [\((k - 1) * ( sqrt D))/] + 1)) & (D is non square implies F is one-to-one)

    proof

      deffunc F( Nat) = ( [\(($1 - 1) * ( sqrt D))/] + 1);

      consider p be FinSequence such that

       A1: ( len p) = (n + 1) & for k st k in ( dom p) holds (p . k) = F(k) from FINSEQ_1:sch 2;

      ( rng p) c= NAT

      proof

        let y be object such that

         A2: y in ( rng p);

        consider x be object such that

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

        reconsider x as Nat by A3;

        1 <= x <= (n + 1) by A3, A1, FINSEQ_3: 25;

        then

         A4: (1 - 1) <= (x - 1) by XREAL_1: 9;

         0 < D or D = 0 ;

        then 0 < ( sqrt D) or ( sqrt D) = 0 by SQUARE_1: 25;

        then 0 <= F(x) by A4, INT_1: 29;

        then F(x) in NAT by INT_1: 3;

        hence thesis by A3, A1;

      end;

      then

      reconsider p as FinSequence of NAT by FINSEQ_1:def 4;

      take p;

      thus ( len p) = (n + 1) & (for k st k in ( dom p) holds (p . k) = ( [\((k - 1) * ( sqrt D))/] + 1)) by A1;

      assume

       A5: D is non square;

      let y1,y2 be object such that

       A6: y1 in ( dom p) & y2 in ( dom p) & (p . y1) = (p . y2);

      assume

       A7: y1 <> y2;

      reconsider y1, y2 as Nat by A6;

      

       A8: (p . y1) = F(y1) & (p . y2) = F(y2) by A6, A1;

      D is non trivial by A5;

      then

       A9: ( sqrt D) > ( sqrt 1) & ( sqrt 1) = 1 by NEWTON03:def 1, SQUARE_1: 18, SQUARE_1: 27;

      per cases by A7, XXREAL_0: 1;

        suppose

         A10: y1 < y2;

        

         A11: ( [\((y2 - 1) * ( sqrt D))/] + 1) <= (((y1 - 1) * ( sqrt D)) + 1) by A6, A8, XREAL_1: 6, INT_1:def 6;

        ((y2 - 1) * ( sqrt D)) < (((y1 - 1) * ( sqrt D)) + 1) by INT_1: 29, A11, XXREAL_0: 2;

        then

         A12: (((y2 - 1) * ( sqrt D)) - ((y1 - 1) * ( sqrt D))) <= 1 by XREAL_1: 19;

        

         A13: ((y2 - y1) * (( sqrt D) / ( sqrt D))) = (((y2 - y1) * ( sqrt D)) / ( sqrt D)) <= (1 / ( sqrt D)) by A12, A9, XREAL_1: 72, XCMPLX_1: 74;

        

         A14: (1 / ( sqrt D)) < (( sqrt D) / ( sqrt D)) & (( sqrt D) / ( sqrt D)) = 1 by XCMPLX_1: 60, A9, XREAL_1: 74;

        

         A15: (y1 - y1) < (y2 - y1) by XREAL_1: 9, A10;

        (y2 - y1) < 1 by XXREAL_0: 2, A13, A14;

        hence contradiction by NAT_1: 14, A15;

      end;

        suppose

         A16: y1 > y2;

        

         A17: ( [\((y1 - 1) * ( sqrt D))/] + 1) <= (((y2 - 1) * ( sqrt D)) + 1) by A6, A8, XREAL_1: 6, INT_1:def 6;

        ((y1 - 1) * ( sqrt D)) < (((y2 - 1) * ( sqrt D)) + 1) by INT_1: 29, A17, XXREAL_0: 2;

        then

         A18: (((y1 - 1) * ( sqrt D)) - ((y2 - 1) * ( sqrt D))) <= 1 by XREAL_1: 19;

        

         A19: ((y1 - y2) * (( sqrt D) / ( sqrt D))) = (((y1 - y2) * ( sqrt D)) / ( sqrt D)) <= (1 / ( sqrt D)) by A18, A9, XREAL_1: 72, XCMPLX_1: 74;

        

         A20: (1 / ( sqrt D)) < (( sqrt D) / ( sqrt D)) & (( sqrt D) / ( sqrt D)) = 1 by XCMPLX_1: 60, A9, XREAL_1: 74;

        

         A21: (y2 - y2) < (y1 - y2) by XREAL_1: 9, A16;

        (y1 - y2) < 1 by XXREAL_0: 2, A19, A20;

        hence contradiction by NAT_1: 14, A21;

      end;

    end;

    theorem :: PELLS_EQ:8

    

     Th8: for a,b be Real, F be FinSequence of REAL st n > 1 & ( len F) = (n + 1) & (for k st k in ( dom F) holds a < (F . k) <= b) holds ex i,j be Nat st i in ( dom F) & j in ( dom F) & i <> j & (F . i) <= (F . j) & ((F . j) - (F . i)) < ((b - a) / n)

    proof

      let a,b be Real, F be FinSequence of REAL such that

       A1: n > 1 & ( len F) = (n + 1) and

       A2: for k st k in ( dom F) holds a < (F . k) <= b;

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

      then 1 in ( dom F) by A1, FINSEQ_3: 25;

      then a < (F . 1) <= b by A2;

      then a < b by XXREAL_0: 2;

      then

       A3: (a - a) < (b - a) by XREAL_1: 9;

      deffunc P( Nat) = ].(a + ((($1 - 1) * (b - a)) / n)), (a + (($1 * (b - a)) / n)).];

      defpred H[ object, object] means for k be Nat st $1 in P(k) holds k = $2;

      

       A4: for x be object st x in ].a, b.] holds ex k be Nat st x in P(k) & k in ( Seg n)

      proof

        let x be object such that

         A5: x in ].a, b.];

        reconsider x as Real by A5;

        set k = [/(((x - a) / (b - a)) * n)\];

        x > a by A5, XXREAL_1: 2;

        then

         A6: (x - a) > 0 by XREAL_1: 50;

        

         A7: k > 0 by INT_1:def 7, A6, A1, A3;

        then

         A8: k >= 1 by NAT_1: 14;

        reconsider k as Element of NAT by A7, INT_1: 3;

        x <= b by A5, XXREAL_1: 2;

        then (x - a) <= (b - a) by XREAL_1: 9;

        then ((x - a) / (b - a)) <= 1 by A6, XREAL_1: 183;

        then

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

        

         A10: ((((x - a) / (b - a)) * n) + 1) <= (n + 1) by XREAL_1: 7, A9;

        k < ((((x - a) / (b - a)) * n) + 1) by INT_1:def 7;

        then k < (n + 1) by A10, XXREAL_0: 2;

        then

         A11: k <= n by NAT_1: 13;

        

         A12: (n / n) = 1 by A1, XCMPLX_1: 60;

        k < ((((x - a) / (b - a)) * n) + 1) by INT_1:def 7;

        then (k - 1) < (((((x - a) / (b - a)) * n) + 1) - 1) by XREAL_1: 9;

        then ((k - 1) / n) < ((((x - a) / (b - a)) * n) / n) by A1, XREAL_1: 74;

        then ((k - 1) / n) < (((x - a) / (b - a)) * 1) by A12, XCMPLX_1: 74;

        then (((k - 1) / n) * (b - a)) < (((x - a) / (b - a)) * (b - a)) by A3, XREAL_1: 68;

        then (((k - 1) / n) * (b - a)) < (((b - a) / (b - a)) * (x - a)) by XCMPLX_1: 75;

        then (((k - 1) / n) * (b - a)) < (1 * (x - a)) by A3, XCMPLX_1: 60;

        then ((((k - 1) / n) * (b - a)) + a) < ((x - a) + a) & (( - a) + a) = 0 by XREAL_1: 6;

        then

         A13: (a + (((k - 1) * (b - a)) / n)) < x by XCMPLX_1: 74;

        (((x - a) / (b - a)) * n) <= k by INT_1:def 7;

        then ((((x - a) / (b - a)) * n) / n) <= (k / n) by XREAL_1: 72;

        then (((x - a) / (b - a)) * 1) <= (k / n) by A12, XCMPLX_1: 74;

        then (((x - a) / (b - a)) * (b - a)) <= ((k / n) * (b - a)) by A3, XREAL_1: 64;

        then (((b - a) / (b - a)) * (x - a)) <= ((k / n) * (b - a)) by XCMPLX_1: 75;

        then (1 * (x - a)) <= ((k / n) * (b - a)) by A3, XCMPLX_1: 60;

        then ((x - a) + a) <= (((k / n) * (b - a)) + a) & (( - a) + a) = 0 by XREAL_1: 6;

        then x <= (a + ((k * (b - a)) / n)) by XCMPLX_1: 74;

        then x in P(k) by A13, XXREAL_1: 2;

        hence thesis by A11, A8, FINSEQ_1: 1;

      end;

      

       A14: for x be object st x in ].a, b.] holds ex y be object st H[x, y]

      proof

        let x be object such that

         A15: x in ].a, b.];

        consider k be Nat such that

         A16: x in P(k) & k in ( Seg n) by A15, A4;

        take y = k;

        let k1 be Nat such that

         A17: x in P(k1);

        reconsider x as Real by A15;

        

         A18: (n / n) = 1 by A1, XCMPLX_1: 60;

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

        then 1 in ( dom F) by A1, FINSEQ_3: 25;

        then a < (F . 1) <= b by A2;

        then a < b by XXREAL_0: 2;

        then

         A19: (a - a) < (b - a) by XREAL_1: 9;

        

         A20: ((b - a) / (b - a)) = 1 by A19, XCMPLX_1: 60;

        (a + (((k1 - 1) * (b - a)) / n)) < x <= (a + ((k * (b - a)) / n)) by XXREAL_1: 2, A16, A17;

        then ((((k1 - 1) * (b - a)) / n) + a) < (((k * (b - a)) / n) + a) by XXREAL_0: 2;

        then

         A21: (((((k1 - 1) * (b - a)) / n) + a) - a) < ((((k * (b - a)) / n) + a) - a) by XREAL_1: 9;

        

         A22: ((((k1 - 1) * (b - a)) / n) * n) = (((k1 - 1) * ((b - a) / n)) * n) by XCMPLX_1: 74

        .= ((k1 - 1) * (((b - a) / n) * n))

        .= ((k1 - 1) * ((n / n) * (b - a))) by XCMPLX_1: 75

        .= ((k1 - 1) * (b - a)) by A18;

        

         A23: (((k * (b - a)) / n) * n) = ((k * ((b - a) / n)) * n) by XCMPLX_1: 74

        .= (k * (((b - a) / n) * n))

        .= (k * ((n / n) * (b - a))) by XCMPLX_1: 75

        .= (k * (b - a)) by A18;

        

         A24: (((k1 - 1) * (b - a)) / (b - a)) = ((k1 - 1) * 1) by A20, XCMPLX_1: 74;

        

         A25: ((k * (b - a)) / (b - a)) = (k * 1) by A20, XCMPLX_1: 74;

        ((k1 - 1) * (b - a)) < (k * (b - a)) by A21, A1, XREAL_1: 68, A22, A23;

        then ((k1 - 1) * 1) < (k * 1) by A24, A25, A19, XREAL_1: 74;

        then ((k1 - 1) + 1) < (k + 1) by XREAL_1: 6;

        then

         A26: k1 <= k by NAT_1: 13;

        (a + (((k - 1) * (b - a)) / n)) < x <= (a + ((k1 * (b - a)) / n)) by XXREAL_1: 2, A16, A17;

        then (a + (((k - 1) * (b - a)) / n)) < (a + ((k1 * (b - a)) / n)) by XXREAL_0: 2;

        then (((((k - 1) * (b - a)) / n) + a) - a) < ((((k1 * (b - a)) / n) + a) - a) by XREAL_1: 9;

        then

         A27: ((((k - 1) * (b - a)) / n) * n) < (((k1 * (b - a)) / n) * n) by A1, XREAL_1: 68;

        

         A28: ((((k - 1) * (b - a)) / n) * n) = (((k - 1) * ((b - a) / n)) * n) by XCMPLX_1: 74

        .= ((k - 1) * (((b - a) / n) * n))

        .= ((k - 1) * ((n / n) * (b - a))) by XCMPLX_1: 75

        .= ((k - 1) * (b - a)) by A18;

        

         A29: (((k1 * (b - a)) / n) * n) = ((k1 * ((b - a) / n)) * n) by XCMPLX_1: 74

        .= (k1 * (((b - a) / n) * n))

        .= (k1 * ((n / n) * (b - a))) by XCMPLX_1: 75

        .= (k1 * (b - a)) by A18;

        

         A30: (((k - 1) * (b - a)) / (b - a)) = ((k - 1) * 1) by A20, XCMPLX_1: 74;

        

         A31: ((k1 * (b - a)) / (b - a)) = (k1 * ((b - a) / (b - a))) by XCMPLX_1: 74

        .= (k1 * 1) by A19, XCMPLX_1: 60;

        ((k - 1) * 1) < (k1 * 1) by A30, A31, A27, A28, A29, A19, XREAL_1: 74;

        then ((k - 1) + 1) < (k1 + 1) by XREAL_1: 6;

        then k <= k1 by NAT_1: 13;

        hence thesis by XXREAL_0: 1, A26;

      end;

      consider f be Function such that

       A32: ( dom f) = ].a, b.] and

       A33: for x be object st x in ].a, b.] holds H[x, (f . x)] from CLASSES1:sch 1( A14);

      set fF = (f * F);

      ( rng F) c= ( dom f)

      proof

        let x be object;

        assume x in ( rng F);

        then

        consider y be object such that

         A34: y in ( dom F) & (F . y) = x by FUNCT_1:def 3;

        reconsider y as Nat by A34;

        a < (F . y) <= b by A2, A34;

        hence x in ( dom f) by A34, A32, XXREAL_1: 2;

      end;

      then

       A35: ( dom fF) = ( dom F) by RELAT_1: 27;

      

       A36: ( rng fF) c= ( Seg n)

      proof

        let x be object;

        assume x in ( rng fF);

        then

        consider y be object such that

         A37: y in ( dom fF) & (fF . y) = x by FUNCT_1:def 3;

        reconsider y as Nat by A37;

        

         A38: (fF . y) = (f . (F . y)) & y in ( dom F) & (F . y) in ( dom f) by FUNCT_1: 11, FUNCT_1: 12, A37;

        consider k be Nat such that

         A39: (F . y) in P(k) & k in ( Seg n) by A38, A32, A4;

        thus thesis by A38, A32, A33, A37, A39;

      end;

      assume

       A40: for n1,n2 be Nat st n1 in ( dom F) & n2 in ( dom F) & n1 <> n2 & (F . n1) <= (F . n2) holds ((F . n2) - (F . n1)) >= ((b - a) / n);

      

       A41: fF is one-to-one

      proof

        let x1,x2 be object such that

         A42: x1 in ( dom fF) & x2 in ( dom fF) & (fF . x1) = (fF . x2);

        assume

         A43: x1 <> x2;

        

         A44: x1 in ( dom F) & (F . x1) in ( dom f) by A42, FUNCT_1: 11;

        

         A45: x2 in ( dom F) & (F . x2) in ( dom f) by A42, FUNCT_1: 11;

        reconsider x1, x2 as Nat by A42;

        

         A46: (fF . x1) = (f . (F . x1)) by A42, FUNCT_1: 12;

        consider k1 be Nat such that

         A47: (F . x1) in P(k1) & k1 in ( Seg n) by A4, A44, A32;

        consider k2 be Nat such that

         A48: (F . x2) in P(k2) & k2 in ( Seg n) by A4, A45, A32;

        k1 = (f . (F . x1)) & k2 = (f . (F . x2)) by A47, A48, A44, A45, A33, A32;

        then

         A49: k1 = k2 by A42, A46, FUNCT_1: 12;

        (F . x1) <= (F . x2) or (F . x2) <= (F . x1);

        then

         A50: ((F . x1) - (F . x2)) >= ((b - a) / n) or ((F . x2) - (F . x1)) >= ((b - a) / n) by A40, A44, A45, A43;

        

         A51: (F . x1) <= (a + ((k1 * (b - a)) / n)) & (F . x2) > (a + (((k1 - 1) * (b - a)) / n)) by A47, A48, A49, XXREAL_1: 2;

        

         A52: ((a + ((k1 * (b - a)) / n)) - (a + (((k1 - 1) * (b - a)) / n))) = (((a + ((k1 * (b - a)) / n)) - a) - (((k1 - 1) * (b - a)) / n))

        .= ((k1 * ((b - a) / n)) - (((k1 - 1) * (b - a)) / n)) by XCMPLX_1: 74

        .= ((k1 * ((b - a) / n)) - ((k1 - 1) * ((b - a) / n))) by XCMPLX_1: 74

        .= ((b - a) / n);

        (F . x2) <= (a + ((k1 * (b - a)) / n)) & (F . x1) > (a + (((k1 - 1) * (b - a)) / n)) by A47, A48, A49, XXREAL_1: 2;

        hence contradiction by A50, A52, A51, XREAL_1: 15;

      end;

      

       A53: ( card ( dom fF)) c= ( card ( rng fF)) by CARD_1: 10, A41;

      ( card ( rng fF)) c= ( card ( Seg n)) by A36, CARD_1: 11;

      then

       A54: ( Segm ( card ( dom fF))) c= ( Segm ( card ( Seg n))) by A53;

      

       A55: ( dom F) = ( Seg (n + 1)) by A1, FINSEQ_1:def 3;

      

       A56: ( card ( Seg n)) = n & ( card ( Seg (n + 1))) = (n + 1) by FINSEQ_1: 57;

      (n + 1) <= n by A56, A54, A55, A35, NAT_1: 39;

      hence contradiction by NAT_1: 13;

    end;

    theorem :: PELLS_EQ:9

    

     Th9: D is non square & n > 1 implies ex x,y be Integer st y <> 0 & |.y.| <= n & 0 < (x - (y * ( sqrt D))) < (1 / n)

    proof

      assume

       A1: D is non square & n > 1;

      consider x be FinSequence of NAT such that

       A2: ( len x) = (n + 1) and

       A3: for k st k in ( dom x) holds (x . k) = ( [\((k - 1) * ( sqrt D))/] + 1) and D is non square implies x is one-to-one by Th7;

      deffunc U( Nat) = ((x . $1) - (($1 - 1) * ( sqrt D)));

      consider u be FinSequence such that

       A4: ( len u) = (n + 1) and

       A5: for k st k in ( dom u) holds (u . k) = U(k) from FINSEQ_1:sch 2;

      ( rng u) c= REAL

      proof

        let y be object;

        assume y in ( rng u);

        then

        consider x be object such that

         A6: x in ( dom u) & (u . x) = y by FUNCT_1:def 3;

        reconsider x as Nat by A6;

        (u . x) = U(x) by A5, A6;

        hence thesis by A6, XREAL_0:def 1;

      end;

      then

      reconsider u as FinSequence of REAL by FINSEQ_1:def 4;

      

       A7: ( dom x) = ( dom u) by A2, A4, FINSEQ_3: 29;

      for k st k in ( dom u) holds 0 < (u . k) <= 1

      proof

        let k such that

         A8: k in ( dom u);

        

         A9: (u . k) = ((x . k) - ((k - 1) * ( sqrt D))) by A8, A5;

        (x . k) = ( [\((k - 1) * ( sqrt D))/] + 1) by A8, A7, A3;

        then (u . k) = (( [\((k - 1) * ( sqrt D))/] - ((k - 1) * ( sqrt D))) + 1) by A9;

        hence thesis by Lm1;

      end;

      then

      consider n1,n2 be Nat such that

       A10: n1 in ( dom u) & n2 in ( dom u) & n1 <> n2 & (u . n1) <= (u . n2) & ((u . n2) - (u . n1)) < ((1 - 0 ) / n) by A1, A4, Th8;

      

       A11: (u . n1) = ((x . n1) - ((n1 - 1) * ( sqrt D))) & (u . n2) = ((x . n2) - ((n2 - 1) * ( sqrt D))) by A5, A10;

      

       A12: (u . n1) <> (u . n2)

      proof

        assume (u . n1) = (u . n2);

        then ((x . n1) + ((1 - n1) * ( sqrt D))) = ((x . n2) + ((1 - n2) * ( sqrt D))) by A11;

        then (1 - n1) = (1 - n2) by A1, Th3;

        hence thesis by A10;

      end;

      set X = ((x . n2) - (x . n1)), Y = (n2 - n1);

      take X, Y;

      1 <= n1 <= (n + 1) & 1 <= n2 <= (n + 1) by A4, A10, FINSEQ_3: 25;

      then (1 - (n + 1)) <= Y <= ((n + 1) - 1) by XREAL_1: 13;

      then

       A13: ( - n) <= Y <= n;

      (u . n2) > (u . n1) by A12, A10, XXREAL_0: 1;

      hence thesis by A13, ABSVALUE: 5, A10, A11, XREAL_1: 50;

    end;

    theorem :: PELLS_EQ:10

    

     Th10: D is non square & n <> 0 & |.y.| <= n & 0 < (x - (y * ( sqrt D))) < (1 / n) implies |.((x ^2 ) - (D * (y ^2 ))).| <= ((2 * ( sqrt D)) + (1 / (n ^2 )))

    proof

      assume that

       A1: D is non square & n <> 0 and

       A2: |.y.| <= n & 0 < (x - (y * ( sqrt D))) < (1 / n);

      

       A3: ( sqrt D) > 0 by A1, SQUARE_1: 25;

      then

       A4: |.( sqrt D).| = ( sqrt D) by ABSVALUE:def 1;

      

       A5: ( - n) <= y <= n by A2, ABSVALUE: 5;

      

       A6: (y * ( sqrt D)) < x < ((1 / n) + (y * ( sqrt D))) by A2, XREAL_1: 19, XREAL_1: 47;

      

       A7: (( - n) * ( sqrt D)) <= (y * ( sqrt D)) <= (n * ( sqrt D)) by XREAL_1: 64, A5, A3;

      then

       A8: ((y * ( sqrt D)) + (1 / n)) <= ((n * ( sqrt D)) + (1 / n)) by XREAL_1: 6;

      ((( - n) * ( sqrt D)) - (1 / n)) <= (( - n) * ( sqrt D)) by XREAL_1: 51;

      then ((( - n) * ( sqrt D)) - (1 / n)) <= (y * ( sqrt D)) by A7, XXREAL_0: 2;

      then ( - ((n * ( sqrt D)) + (1 / n))) < x < ((n * ( sqrt D)) + (1 / n)) by A6, A8, XXREAL_0: 2;

      then

       A9: |.x.| <= ((n * ( sqrt D)) + (1 / n)) by ABSVALUE: 5;

      

       A10: ( |.y.| * |.( sqrt D).|) <= (n * |.( sqrt D).|) by A2, XREAL_1: 64, A3, A4;

       |.(x + (y * ( sqrt D))).| <= ( |.x.| + |.(y * ( sqrt D)).|) by COMPLEX1: 56;

      then

       A11: |.(x + (y * ( sqrt D))).| <= ( |.x.| + ( |.y.| * ( sqrt D))) by A4, COMPLEX1: 65;

      ( |.x.| + ( |.y.| * ( sqrt D))) <= (((n * ( sqrt D)) + (1 / n)) + (n * ( sqrt D))) by A4, A9, A10, XREAL_1: 7;

      then

       A12: 0 <= |.(x + (y * ( sqrt D))).| <= (((2 * n) * ( sqrt D)) + (1 / n)) by COMPLEX1: 46, A11, XXREAL_0: 2;

      ( - (1 / n)) <= 0 <= (x - (y * ( sqrt D))) <= (1 / n) by A2;

      then

       A13: 0 <= |.(x - (y * ( sqrt D))).| <= (1 / n) by ABSVALUE: 5;

      

       A14: ((2 * n) / n) = 2 by A1, XCMPLX_1: 89;

      ( |.(x + (y * ( sqrt D))).| * |.(x - (y * ( sqrt D))).|) <= ((((2 * n) * ( sqrt D)) + (1 / n)) * (1 / n)) by XREAL_1: 66, A12, A13;

      then ( |.(x + (y * ( sqrt D))).| * |.(x - (y * ( sqrt D))).|) <= ((((2 * n) * (1 / n)) * ( sqrt D)) + ((1 / n) * (1 / n)));

      then ( |.(x + (y * ( sqrt D))).| * |.(x - (y * ( sqrt D))).|) <= ((((2 * n) / n) * ( sqrt D)) + ((1 / n) * (1 / n))) by XCMPLX_1: 99;

      then ( |.(x + (y * ( sqrt D))).| * |.(x - (y * ( sqrt D))).|) <= (((2 * 1) * ( sqrt D)) + ((1 * 1) / (n * n))) by XCMPLX_1: 76, A14;

      then |.((x + (y * ( sqrt D))) * (x - (y * ( sqrt D)))).| <= ((2 * ( sqrt D)) + (1 / (n * n))) by COMPLEX1: 65;

      then |.((x ^2 ) - ((y ^2 ) * (( sqrt D) ^2 ))).| <= ((2 * ( sqrt D)) + (1 / (n * n)));

      then |.((x ^2 ) - ((y ^2 ) * ( sqrt (D ^2 )))).| <= ((2 * ( sqrt D)) + (1 / (n * n))) by SQUARE_1: 29;

      hence thesis by SQUARE_1: 22;

    end;

    theorem :: PELLS_EQ:11

    

     Th11: D is non square implies ex x,y be Integer st y <> 0 & 0 < (x - (y * ( sqrt D))) & |.((x ^2 ) - (D * (y ^2 ))).| < ((2 * ( sqrt D)) + 1)

    proof

      assume

       A1: D is non square;

      then

      consider x,y be Integer such that

       A2: y <> 0 and

       A3: |.y.| <= 2 and

       A4: 0 < (x - (y * ( sqrt D))) < (1 / 2) by Th9;

      

       A5: |.((x ^2 ) - (D * (y ^2 ))).| <= ((2 * ( sqrt D)) + (1 / (2 ^2 ))) by A1, A3, A4, Th10;

      take x, y;

      ((2 * ( sqrt D)) + (1 / (2 ^2 ))) < ((2 * ( sqrt D)) + 1) by XREAL_1: 6;

      hence thesis by A2, A4, A5, XXREAL_0: 2;

    end;

    theorem :: PELLS_EQ:12

    

     Th12: D is non square implies { [x, y] where x,y be Integer : y <> 0 & |.((x ^2 ) - (D * (y ^2 ))).| < ((2 * ( sqrt D)) + 1) & 0 < (x - (y * ( sqrt D))) } is infinite

    proof

      set S = { [x, y] where x,y be Integer : y <> 0 & |.((x ^2 ) - (D * (y ^2 ))).| < ((2 * ( sqrt D)) + 1) & 0 < (x - (y * ( sqrt D))) };

      assume

       A1: D is non square & S is finite;

      ex f be Function of S, REAL st for x,y be Integer st [x, y] in S holds (f . [x, y]) = (x - (y * ( sqrt D)))

      proof

        defpred P[ object, object] means for x,y be Integer st [x, y] = $1 holds $2 = (x - (y * ( sqrt D)));

        

         A2: for xy be object st xy in S holds ex u be object st P[xy, u]

        proof

          let xy be object such that

           A3: xy in S;

          consider x,y be Integer such that

           A4: xy = [x, y] & y <> 0 & |.((x ^2 ) - (D * (y ^2 ))).| < ((2 * ( sqrt D)) + 1) & 0 < (x - (y * ( sqrt D))) by A3;

          take u = (x - (y * ( sqrt D)));

          let x1,y1 be Integer such that

           A5: [x1, y1] = xy;

          x1 = x & y1 = y by A4, A5, XTUPLE_0: 1;

          hence thesis;

        end;

        consider f be Function such that

         A6: ( dom f) = S & for xy be object st xy in S holds P[xy, (f . xy)] from CLASSES1:sch 1( A2);

        ( rng f) c= REAL

        proof

          let a be object;

          assume a in ( rng f);

          then

          consider xy be object such that

           A7: xy in ( dom f) & (f . xy) = a by FUNCT_1:def 3;

          consider x be Integer, y be Integer such that

           A8: xy = [x, y] & y <> 0 & |.((x ^2 ) - (D * (y ^2 ))).| < ((2 * ( sqrt D)) + 1) & 0 < (x - (y * ( sqrt D))) by A6, A7;

          (f . xy) = (x - (y * ( sqrt D))) by A6, A7, A8;

          hence a in REAL by A7, XREAL_0:def 1;

        end;

        then

        reconsider f as Function of S, REAL by A6, FUNCT_2: 2;

        take f;

        thus thesis by A6;

      end;

      then

      consider f be Function of S, REAL such that

       A9: for x,y be Integer st [x, y] in S holds (f . [x, y]) = (x - (y * ( sqrt D)));

      S is non empty

      proof

        consider x,y be Integer such that

         A10: y <> 0 & 0 < (x - (y * ( sqrt D))) & |.((x ^2 ) - (D * (y ^2 ))).| < ((2 * ( sqrt D)) + 1) by A1, Th11;

         [x, y] in S by A10;

        hence thesis;

      end;

      then

      reconsider R = ( rng f) as finite non empty Subset of REAL by A1;

      ( inf R) > 0

      proof

        ( min R) in R by XXREAL_2:def 7;

        then

        consider xy be object such that

         A11: xy in ( dom f) & (f . xy) = ( inf R) by FUNCT_1:def 3;

        xy in S by A11;

        then ex x be Integer, y be Integer st xy = [x, y] & y <> 0 & |.((x ^2 ) - (D * (y ^2 ))).| < ((2 * ( sqrt D)) + 1) & 0 < (x - (y * ( sqrt D)));

        hence thesis by A9, A11;

      end;

      then

      consider n be Nat such that

       A12: (1 / n) < ( inf R) and

       A13: n > 1 by Lm3;

      consider x,y be Integer such that

       A14: y <> 0 & |.y.| <= n & 0 < (x - (y * ( sqrt D))) < (1 / n) by A1, A13, Th9;

      

       A15: |.((x ^2 ) - (D * (y ^2 ))).| <= ((2 * ( sqrt D)) + (1 / (n ^2 ))) by A1, A13, A14, Th10;

      ((2 * ( sqrt D)) + (1 / (n ^2 ))) < ((2 * ( sqrt D)) + 1)

      proof

        (n * n) > (1 * 1) by A13, XREAL_1: 96;

        then (1 / (n * n)) < 1 by XREAL_1: 189;

        hence thesis by XREAL_1: 6;

      end;

      then |.((x ^2 ) - (D * (y ^2 ))).| < ((2 * ( sqrt D)) + 1) by A15, XXREAL_0: 2;

      then [x, y] in S & S = ( dom f) by A14, FUNCT_2:def 1;

      then (f . [x, y]) in R & (f . [x, y]) = (x - (y * ( sqrt D))) by A9, FUNCT_1:def 3;

      then (x - (y * ( sqrt D))) >= ( inf R) by XXREAL_2:def 7;

      hence contradiction by A12, A14, XXREAL_0: 2;

    end;

    theorem :: PELLS_EQ:13

    

     Th13: D is non square implies ex k,a,b,c,d be Integer st 0 <> k & ((a ^2 ) - (D * (b ^2 ))) = k = ((c ^2 ) - (D * (d ^2 ))) & (a,c) are_congruent_mod k & (b,d) are_congruent_mod k & ( |.a.| <> |.c.| or |.b.| <> |.d.|)

    proof

      set S = { [x, y] where x be Integer, y be Integer : y <> 0 & |.((x ^2 ) - (D * (y ^2 ))).| < ((2 * ( sqrt D)) + 1) & 0 < (x - (y * ( sqrt D))) };

      assume

       A1: D is non square;

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

      then

      reconsider M = [/((2 * ( sqrt D)) + 1)\] as Element of NAT by INT_1: 53;

      defpred P[ object, object] means for x,y be Integer st [x, y] = $1 holds $2 = ((x ^2 ) - (D * (y ^2 )));

      

       A2: for xy be object st xy in S holds ex u be object st P[xy, u]

      proof

        let xy be object such that

         A3: xy in S;

        consider x,y be Integer such that

         A4: xy = [x, y] & y <> 0 & |.((x ^2 ) - (D * (y ^2 ))).| < ((2 * ( sqrt D)) + 1) & 0 < (x - (y * ( sqrt D))) by A3;

        take u = ((x ^2 ) - (D * (y ^2 )));

        let x1,y1 be Integer such that

         A5: [x1, y1] = xy;

        x1 = x & y1 = y by A4, A5, XTUPLE_0: 1;

        hence thesis;

      end;

      consider f be Function such that

       A6: ( dom f) = S & for xy be object st xy in S holds P[xy, (f . xy)] from CLASSES1:sch 1( A2);

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

      then

      reconsider M = [/((2 * ( sqrt D)) + 1)\] as Element of NAT by INT_1: 53;

      defpred P[ Integer] means $1 <> 0 ;

      deffunc F( set) = $1;

      set SS = { F(i) where i be Element of INT : ( - M) <= i & i <= M & P[i] };

      SS is finite from XXREAL_2:sch 1;

      then

      reconsider SS as finite set;

      

       A7: ( rng f) c= SS

      proof

        let r be object;

        assume r in ( rng f);

        then

        consider xy be object such that

         A8: xy in ( dom f) & (f . xy) = r by FUNCT_1:def 3;

        consider x,y be Integer such that

         A9: xy = [x, y] & y <> 0 & |.((x ^2 ) - (D * (y ^2 ))).| < ((2 * ( sqrt D)) + 1) & 0 < (x - (y * ( sqrt D))) by A8, A6;

        

         A10: (f . xy) = ((x ^2 ) - (D * (y ^2 ))) by A8, A9, A6;

        then

        reconsider r as Element of INT by A8, INT_1:def 2;

        

         A11: P[r] by A8, A9, A1, A10;

        ((2 * ( sqrt D)) + 1) <= M by INT_1:def 7;

        then |.r.| < M by A8, A9, A10, XXREAL_0: 2;

        then ( - M) <= r <= M by ABSVALUE: 5;

        hence thesis by A11;

      end;

      then

      consider k1 be object such that

       A12: k1 in ( rng f) & (f " {k1}) is infinite by A1, Th12, A6, CARD_2: 101;

      k1 in SS by A12, A7;

      then

      consider k be Element of INT such that

       A13: k = k1 & ( - M) <= k <= M & P[k];

      set Z = (f " {k});

      take k;

      

       A14: Z c= S by RELAT_1: 132, A6;

      defpred R[ object, object] means for x,y be Integer st [x, y] = $1 holds $2 = [(x mod k), (y mod k)];

      

       A15: for xy be object st xy in Z holds ex u be object st R[xy, u]

      proof

        let xy be object such that

         A16: xy in Z;

        xy in S by A16, A14;

        then

        consider x,y be Integer such that

         A17: xy = [x, y] & y <> 0 & |.((x ^2 ) - (D * (y ^2 ))).| < ((2 * ( sqrt D)) + 1) & 0 < (x - (y * ( sqrt D)));

        take u = [(x mod k), (y mod k)];

        let x1,y1 be Integer such that

         A18: [x1, y1] = xy;

        x1 = x & y1 = y by A17, A18, XTUPLE_0: 1;

        hence thesis;

      end;

      consider g be Function such that

       A19: ( dom g) = Z & for xy be object st xy in Z holds R[xy, (g . xy)] from CLASSES1:sch 1( A15);

      defpred R[ object] means not contradiction;

      set K = { F(i) where i be Element of INT : ( - |.k.|) <= i & i <= |.k.| & R[i] };

      

       A20: K is finite from XXREAL_2:sch 1;

      ( rng g) c= [:K, K:]

      proof

        let b be object;

        assume b in ( rng g);

        then

        consider a be object such that

         A21: a in ( dom g) & (g . a) = b by FUNCT_1:def 3;

        a in ( dom f) & (f . a) in {k} by A19, A21, FUNCT_1:def 7;

        then

        consider x,y be Integer such that

         A22: a = [x, y] & y <> 0 & |.((x ^2 ) - (D * (y ^2 ))).| < ((2 * ( sqrt D)) + 1) & 0 < (x - (y * ( sqrt D))) by A6;

        

         A23: (g . a) = [(x mod k), (y mod k)] by A22, A21, A19;

        

         A24: (x mod k) in INT by INT_1:def 2;

         |.(x mod k).| < |.k.| by Th2, A13;

        then ( - |.k.|) <= (x mod k) <= |.k.| by ABSVALUE: 5;

        then

         A25: (x mod k) in K by A24;

        

         A26: (y mod k) in INT by INT_1:def 2;

         |.(y mod k).| < |.k.| by Th2, A13;

        then ( - |.k.|) <= (y mod k) <= |.k.| by ABSVALUE: 5;

        then (y mod k) in K by A26;

        hence b in [:K, K:] by A21, A23, A25, ZFMISC_1: 87;

      end;

      then

      consider ab be object such that

       A27: ab in ( rng g) & (g " {ab}) is infinite by A19, A12, A13, A20, CARD_2: 101;

      consider X be object such that

       A28: X in (g " {ab}) by A27, XBOOLE_0:def 1;

      

       A29: X in ( dom g) & (g . X) in {ab} by A28, FUNCT_1:def 7;

      

       A30: X in ( dom f) & (f . X) in {k} by A29, A19, FUNCT_1:def 7;

      then

      consider x,y be Integer such that

       A31: X = [x, y] & y <> 0 & |.((x ^2 ) - (D * (y ^2 ))).| < ((2 * ( sqrt D)) + 1) & 0 < (x - (y * ( sqrt D))) by A6;

      

       A32: (g . X) = [(x mod k), (y mod k)] by A31, A29, A19;

      ex a,b,c,d be Integer st ((a ^2 ) - (D * (b ^2 ))) = k = ((c ^2 ) - (D * (d ^2 ))) & (a,c) are_congruent_mod k & (b,d) are_congruent_mod k & ( |.a.| <> |.c.| or |.b.| <> |.d.|)

      proof

        assume

         A33: for a,b,c,d be Integer st ((a ^2 ) - (D * (b ^2 ))) = k = ((c ^2 ) - (D * (d ^2 ))) & (a,c) are_congruent_mod k & (b,d) are_congruent_mod k holds |.a.| = |.c.| & |.b.| = |.d.|;

        (g " {ab}) c= { [x, y], [( - x), y], [x, ( - y)], [( - x), ( - y)]}

        proof

          let Y be object;

          assume Y in (g " {ab});

          then

           A34: Y in ( dom g) & (g . Y) in {ab} by FUNCT_1:def 7;

          then

           A35: Y in ( dom f) & (f . Y) in {k} by A19, FUNCT_1:def 7;

          then

          consider x1,y1 be Integer such that

           A36: Y = [x1, y1] & y1 <> 0 & |.((x1 ^2 ) - (D * (y1 ^2 ))).| < ((2 * ( sqrt D)) + 1) & 0 < (x1 - (y1 * ( sqrt D))) by A6;

          

           A37: (g . X) = ab = (g . Y) by A29, A34, TARSKI:def 1;

          (g . Y) = [(x1 mod k), (y1 mod k)] by A36, A34, A19;

          then

           A38: (x mod k) = (x1 mod k) & (y mod k) = (y1 mod k) by A32, A37, XTUPLE_0: 1;

          

           A39: (x,x1) are_congruent_mod k

          proof

            x = (((x div k) * k) + (x mod k)) & x1 = (((x1 div k) * k) + (x1 mod k)) by INT_1: 59, A13;

            then (x - x1) = (k * ((x div k) - (x1 div k))) by A38;

            hence thesis by INT_1:def 5;

          end;

          

           A40: (y,y1) are_congruent_mod k

          proof

            y = (((y div k) * k) + (y mod k)) & y1 = (((y1 div k) * k) + (y1 mod k)) by INT_1: 59, A13;

            then (y - y1) = (k * ((y div k) - (y1 div k))) by A38;

            hence thesis by INT_1:def 5;

          end;

          (f . X) = k = (f . Y) by A30, A35, TARSKI:def 1;

          then ((x1 ^2 ) - (D * (y1 ^2 ))) = k = ((x ^2 ) - (D * (y ^2 ))) by A36, A35, A30, A31, A6;

          then |.x.| = |.x1.| & |.y.| = |.y1.| by A33, A39, A40;

          then (x = x1 or x = ( - x1)) & (y = y1 or y = ( - y1)) by ABSVALUE: 28;

          hence thesis by A36, ENUMSET1:def 2;

        end;

        hence contradiction by A27;

      end;

      hence thesis by A13;

    end;

    begin

    ::$Notion-Name

    theorem :: PELLS_EQ:14

    

     Th14: D is non square implies ex x,y be Nat st ((x ^2 ) - (D * (y ^2 ))) = 1 & y <> 0

    proof

      assume D is non square;

      then

      consider k,a,b,c,d be Integer such that

       A1: 0 <> k and

       A2: ((a ^2 ) - (D * (b ^2 ))) = k = ((c ^2 ) - (D * (d ^2 ))) and

       A3: (a,c) are_congruent_mod k and

       A4: (b,d) are_congruent_mod k and

       A5: |.a.| <> |.c.| or |.b.| <> |.d.| by Th13;

      consider t be Integer such that

       A6: (a - c) = (k * t) by A3, INT_1:def 5;

      consider v be Integer such that

       A7: (b - d) = (k * v) by A4, INT_1:def 5;

      reconsider x = |.((1 + (c * t)) - ((D * d) * v)).|, y = |.((d * t) - (c * v)).| as Nat by TARSKI: 1;

      take x, y;

      

       A8: a = (c + (k * t)) & b = (d + (k * v)) by A6, A7;

      

       A9: ((a * c) - ((D * b) * d)) = (((c + (k * t)) * c) - ((D * (d + (k * v))) * d)) by A6, A7

      .= (((c ^2 ) - (D * (d ^2 ))) + (k * ((c * t) - ((D * d) * v))))

      .= (k * ((1 + (c * t)) - ((D * d) * v))) by A2;

      

       A10: ((((a * c) - ((D * b) * d)) ^2 ) - (D * (((a * d) - (c * b)) ^2 ))) = ((((a * c) - ((D * b) * d)) ^2 ) - (D * ((((c + (k * t)) * d) - ((d + (k * v)) * c)) ^2 ))) by A6, A7

      .= (((k * ((1 + (c * t)) - ((D * d) * v))) ^2 ) - (D * ((k * ((d * t) - (c * v))) ^2 ))) by A9;

      (x ^2 ) = (((1 + (c * t)) - ((D * d) * v)) ^2 ) & (y ^2 ) = (((d * t) - (c * v)) ^2 ) by COMPLEX1: 75;

      

      hence

       A11: ((x ^2 ) - (D * (y ^2 ))) = ((((((1 + (c * t)) - ((D * d) * v)) ^2 ) * (k ^2 )) - ((D * (((d * t) - (c * v)) ^2 )) * (k ^2 ))) / (k ^2 )) by A1, XCMPLX_1: 129

      .= ((((a ^2 ) - (D * (b ^2 ))) * ((c ^2 ) - (D * (d ^2 )))) / (k ^2 )) by A10

      .= 1 by A2, A1, XCMPLX_1: 60;

      assume

       A12: y = 0 ;

      

       A13: (((1 + (c * t)) - ((D * d) * v)) * c) = ((c + ((c * t) * c)) - ((D * d) * ( 0 + (v * c))))

      .= ((c + ((c * t) * c)) - ((D * d) * (((d * t) - (c * v)) + (v * c)))) by A12, ABSVALUE: 2

      .= (c + (((c ^2 ) - (D * (d ^2 ))) * t));

      

       A14: (((1 + (c * t)) - ((D * d) * v)) * d) = (((1 * d) + (c * ((t * d) - 0 ))) - (((D * d) * v) * d))

      .= (((1 * d) + (c * ((t * d) - ((d * t) - (c * v))))) - (((D * d) * v) * d)) by A12, ABSVALUE: 2

      .= (d + (((c ^2 ) - (D * (d ^2 ))) * v));

      

       A15: x = 1 by A11, A12, SQUARE_1: 18, SQUARE_1: 22;

      per cases by A15, ABSVALUE:def 1;

        suppose ((1 + (c * t)) - ((D * d) * v)) = 1;

        hence contradiction by A5, A2, A8, A13, A14;

      end;

        suppose ( - ((1 + (c * t)) - ((D * d) * v))) = 1;

        then (( - 1) * c) = (c + (((c ^2 ) - (D * (d ^2 ))) * t)) & (( - 1) * d) = (d + (((c ^2 ) - (D * (d ^2 ))) * v)) by A13, A14;

        then ( - c) = (c + (((c ^2 ) - (D * (d ^2 ))) * t)) & ( - d) = (d + (((c ^2 ) - (D * (d ^2 ))) * v));

        hence contradiction by A5, A2, Lm2, A8;

      end;

    end;

    definition

      let D be Nat;

      :: PELLS_EQ:def1

      mode Pell's_solution of D -> Element of [: INT , INT :] means

      : Def1: (((it `1 ) ^2 ) - (D * ((it `2 ) ^2 ))) = 1;

      existence

      proof

        1 in INT & 0 in INT by INT_1:def 2;

        then

        reconsider s = [1, 0 ] as Element of [: INT , INT :] by ZFMISC_1: 87;

        take s;

        thus thesis;

      end;

    end

    

     Lm4: ((x ^2 ) - (D * (y ^2 ))) = 1 iff [x, y] is Pell's_solution of D

    proof

      

       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, Def1;

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

      hence thesis by Def1, A1;

    end;

    definition

      let D1,D2 be real-membered non empty set;

      let p be Element of [:D1, D2:];

      :: PELLS_EQ:def2

      attr p is positive means

      : Def2: (p `1 ) is positive & (p `2 ) is positive;

    end

    registration

      cluster positive for Element of [: INT , INT :];

      existence

      proof

        1 in INT by INT_1:def 2;

        then

        reconsider s = [1, 1] as Element of [: INT , INT :] by ZFMISC_1: 87;

        take s;

        thus thesis;

      end;

    end

    registration

      let p be positive Element of [: INT , INT :];

      cluster (p `1 ) -> positive;

      coherence by Def2;

      cluster (p `2 ) -> positive;

      coherence by Def2;

    end

    theorem :: PELLS_EQ:15

    for D be square Nat, p be positive Element of [: INT , INT :] st D > 0 holds not p is Pell's_solution of D

    proof

      let n be square Nat;

      consider m be Nat such that

       A1: n = (m ^2 ) by PYTHTRIP:def 3;

      let p be positive Element of [: INT , INT :];

      set p1 = (p `1 ), p2 = (p `2 );

      assume

       A2: n > 0 & p is Pell's_solution of n;

      then ((p1 ^2 ) - (n * (p2 ^2 ))) = 1 by Def1;

      then

       A3: ((p1 - (m * p2)) * (p1 + (m * p2))) = 1 by A1;

      per cases by A3, INT_1: 9;

        suppose

         A4: (p1 - (m * p2)) = 1 & (p1 + (m * p2)) = 1;

        (m * p2) >= (1 * m) by NAT_1: 14, XREAL_1: 64;

        hence contradiction by A4, A1, A2;

      end;

        suppose (p1 - (m * p2)) = ( - 1) & (p1 + (m * p2)) = ( - 1);

        hence contradiction;

      end;

    end;

    theorem :: PELLS_EQ:16

    

     Th16: D is non square implies ex p be Pell's_solution of D st p is positive

    proof

      assume D is non square;

      then

      consider x,y be Nat such that

       A1: ((x ^2 ) - (D * (y ^2 ))) = 1 & y <> 0 by Th14;

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

      then

      reconsider ab = [x, y] as Element of [: INT , INT :] by ZFMISC_1: 87;

      x = (ab `1 ) & y = (ab `2 );

      then

      reconsider ab as Pell's_solution of D by A1, Def1;

      take ab;

      thus thesis by A1;

    end;

    registration

      let D be non square Nat;

      cluster positive for Pell's_solution of D;

      existence by Th16;

    end

    ::$Notion-Name

    theorem :: PELLS_EQ:17

    for D be non square Nat holds the set of all ab where ab be positive Pell's_solution of D is infinite

    proof

      let D be non square Nat;

      set P = the set of all ab where ab be positive Pell's_solution of D;

      assume

       A1: P is finite;

      set ab = the positive Pell's_solution of D;

      

       A2: ab = [(ab `1 ), (ab `2 )] & ab in P;

      ( proj2 P) c= NAT

      proof

        let y be object;

        assume y in ( proj2 P);

        then

        consider x be object such that

         A3: [x, y] in P by XTUPLE_0:def 13;

        consider ab be positive Pell's_solution of D such that

         A4: [x, y] = ab by A3;

        y = (ab `2 ) & (ab `2 ) > 0 by A4;

        hence thesis by INT_1: 3;

      end;

      then

      reconsider P2 = ( proj2 P) as finite non empty Subset of NAT by A1, WAYBEL26: 39, A2, XTUPLE_0:def 13;

      set b = ( max P2);

      b in P2 by XXREAL_2:def 8;

      then

      consider a be object such that

       A5: [a, b] in P by XTUPLE_0:def 13;

      consider ab be positive Pell's_solution of D such that

       A6: [a, b] = ab by A5;

      

       A7: a = (ab `1 ) & b = (ab `2 ) by A6;

      then

      reconsider a, b as Nat;

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

      ((a ^2 ) - ((b ^2 ) * D)) = 1 by Lm4, A6;

      then (a ^2 ) = (1 + ((b ^2 ) * D));

      

      then 1 = (((((4 * (a ^2 )) * (a ^2 )) - (4 * (a ^2 ))) + 1) - (((4 * (a ^2 )) * (b ^2 )) * D))

      .= ((A ^2 ) - ((B ^2 ) * D));

      then

      reconsider AB = [A, B] as Pell's_solution of D by Lm4;

      (a ^2 ) >= 1 by A7, NAT_1: 14;

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

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

      then (AB `1 ) > 0 & (AB `2 ) > 0 by A7;

      then AB is positive Pell's_solution of D by Def2;

      then AB in P;

      then

       A8: B in P2 by XTUPLE_0:def 13;

      a >= 1 by A7, NAT_1: 14;

      then (a + a) > (1 + 0 ) by XREAL_1: 8;

      then B > (1 * b) by A7, XREAL_1: 68;

      hence thesis by A8, XXREAL_2:def 8;

    end;

    begin

    reserve p,p1,p2 for Pell's_solution of D;

    theorem :: PELLS_EQ:18

    

     Th18: D is non square implies (p is positive iff ((p `1 ) + ((p `2 ) * ( sqrt D))) > 1)

    proof

      assume

       A1: D is non square;

      thus p is positive implies ((p `1 ) + ((p `2 ) * ( sqrt D))) > 1

      proof

        assume

         A2: p is positive;

        

         A3: (1 ^2 ) = 1;

        

         A4: ( sqrt D) > 1 by A1, SQUARE_1: 27, NAT_1: 25, SQUARE_1: 18, A3;

        (p `2 ) >= ( 0 + 1) by A2, INT_1: 7;

        then

         A5: ((p `2 ) * ( sqrt D)) >= (1 * ( sqrt D)) by A4, XREAL_1: 64;

        ((p `2 ) * ( sqrt D)) > 1 by XXREAL_0: 2, A5, A4;

        then (((p `2 ) * ( sqrt D)) + (p `1 )) > (1 + 0 ) by XREAL_1: 8, A2;

        hence thesis;

      end;

      assume

       A6: ((p `1 ) + ((p `2 ) * ( sqrt D))) > 1;

      

       A7: ( sqrt D) > 0 by A1, SQUARE_1: 25;

      (((p `1 ) ^2 ) - (D * ((p `2 ) ^2 ))) = (((p `1 ) ^2 ) - ((( sqrt D) ^2 ) * ((p `2 ) ^2 ))) by SQUARE_1:def 2;

      then

       A8: (((p `1 ) + ((p `2 ) * ( sqrt D))) * ((p `1 ) - ((p `2 ) * ( sqrt D)))) = (1 * 1) by Def1;

      then

       A9: ((p `1 ) - ((p `2 ) * ( sqrt D))) > 0 & ((p `1 ) - ((p `2 ) * ( sqrt D))) < 1 by A6, XREAL_1: 98;

      (((p `1 ) - ((p `2 ) * ( sqrt D))) + ((p `2 ) * ( sqrt D))) < (1 + ((p `2 ) * ( sqrt D))) by A9, XREAL_1: 8;

      then ((p `1 ) - (p `1 )) < ((1 + ((p `2 ) * ( sqrt D))) - (p `1 )) by XREAL_1: 14;

      then ( 0 - 1) < (((1 + ((p `2 ) * ( sqrt D))) - (p `1 )) - 1) by XREAL_1: 14;

      then ((((p `2 ) * ( sqrt D)) - (p `1 )) + ((p `1 ) + ((p `2 ) * ( sqrt D)))) > (( - 1) + 1) by A6, XREAL_1: 8;

      then (((2 * (p `2 )) * ( sqrt D)) / 2) > ( 0 / 2);

      hence p is positive by A7, A6, A8;

    end;

    theorem :: PELLS_EQ:19

    

     Th19: 1 < ((p1 `1 ) + ((p1 `2 ) * ( sqrt D))) < ((p2 `1 ) + ((p2 `2 ) * ( sqrt D))) & D is non square implies (p1 `1 ) < (p2 `1 ) & (p1 `2 ) < (p2 `2 )

    proof

      assume

       A1: 1 < ((p1 `1 ) + ((p1 `2 ) * ( sqrt D))) < ((p2 `1 ) + ((p2 `2 ) * ( sqrt D))) & D is non square & ((p1 `1 ) >= (p2 `1 ) or (p1 `2 ) >= (p2 `2 ));

      per cases by A1;

        suppose

         A2: (p1 `2 ) >= (p2 `2 );

        

         A3: ( sqrt D) > 0 by A1, SQUARE_1: 25;

        

         A4: p1 is positive by Th18, A1;

        ((p2 `1 ) + ((p2 `2 ) * ( sqrt D))) > 1 by A1, XXREAL_0: 2;

        then

         A5: p2 is positive by Th18, A1;

        ((((p1 `1 ) ^2 ) - (((p1 `2 ) ^2 ) * D)) + (((p1 `2 ) ^2 ) * D)) = (1 + (((p1 `2 ) ^2 ) * D)) by Def1;

        then

         A6: (p1 `1 ) = ( sqrt (1 + (((p1 `2 ) ^2 ) * D))) by SQUARE_1:def 2, A4;

        ((((p2 `1 ) ^2 ) - (((p2 `2 ) ^2 ) * D)) + (((p2 `2 ) ^2 ) * D)) = (1 + (((p2 `2 ) ^2 ) * D)) by Def1;

        then

         A7: (p2 `1 ) = ( sqrt (1 + (((p2 `2 ) ^2 ) * D))) by SQUARE_1:def 2, A5;

        ((p1 `2 ) ^2 ) >= ((p2 `2 ) ^2 ) by SQUARE_1: 15, A5, A2;

        then (((p1 `2 ) ^2 ) * D) >= (((p2 `2 ) ^2 ) * D) by XREAL_1: 64;

        then ((((p1 `2 ) ^2 ) * D) + 1) >= ((((p2 `2 ) ^2 ) * D) + 1) by XREAL_1: 6;

        then

         A8: (p1 `1 ) >= (p2 `1 ) by A6, A7, SQUARE_1: 26;

        ((p1 `2 ) * ( sqrt D)) >= ((p2 `2 ) * ( sqrt D)) by A2, XREAL_1: 64, A3;

        hence contradiction by A1, A8, XREAL_1: 7;

      end;

        suppose

         A9: (p1 `1 ) >= (p2 `1 );

        

         A10: ( sqrt D) > 0 by A1, SQUARE_1: 25;

        

         A11: p1 is positive by Th18, A1;

        ((p2 `1 ) + ((p2 `2 ) * ( sqrt D))) > 1 by A1, XXREAL_0: 2;

        then

         A12: p2 is positive by Th18, A1;

        

         A13: ((((p1 `1 ) ^2 ) - (((p1 `2 ) ^2 ) * D)) + (((p1 `2 ) ^2 ) * D)) = (1 + (((p1 `2 ) ^2 ) * D)) by Def1;

        

         A14: (p1 `1 ) = ( sqrt (1 + (((p1 `2 ) ^2 ) * D))) by A13, SQUARE_1:def 2, A11;

        

         A15: ((((p2 `1 ) ^2 ) - (((p2 `2 ) ^2 ) * D)) + (((p2 `2 ) ^2 ) * D)) = (1 + (((p2 `2 ) ^2 ) * D)) by Def1;

        

         A16: (p2 `1 ) = ( sqrt (1 + (((p2 `2 ) ^2 ) * D))) by A15, SQUARE_1:def 2, A12;

        ( sqrt (1 + (((p1 `2 ) ^2 ) * D))) >= 0 & ( sqrt (1 + (((p2 `2 ) ^2 ) * D))) >= 0 by SQUARE_1: 25;

        then

         A17: (( sqrt (1 + (((p1 `2 ) ^2 ) * D))) ^2 ) >= (( sqrt (1 + (((p2 `2 ) ^2 ) * D))) ^2 ) by SQUARE_1: 15, A9, A14, A16;

        (( sqrt (1 + (((p2 `2 ) ^2 ) * D))) * ( sqrt (1 + (((p2 `2 ) ^2 ) * D)))) = ( sqrt ((1 + (((p2 `2 ) ^2 ) * D)) * (1 + (((p2 `2 ) ^2 ) * D)))) by SQUARE_1: 29;

        then

         A18: ( sqrt ((1 + (((p1 `2 ) ^2 ) * D)) ^2 )) >= ( sqrt ((1 + (((p2 `2 ) ^2 ) * D)) ^2 )) by A17, SQUARE_1: 29;

        

         A19: ( sqrt ((1 + (((p1 `2 ) ^2 ) * D)) ^2 )) = (1 + (((p1 `2 ) ^2 ) * D)) by SQUARE_1: 22;

        ( sqrt ((1 + (((p2 `2 ) ^2 ) * D)) ^2 )) = (1 + (((p2 `2 ) ^2 ) * D)) by SQUARE_1: 22;

        then ((1 + (((p1 `2 ) ^2 ) * D)) - 1) >= ((1 + (((p2 `2 ) ^2 ) * D)) - 1) by XREAL_1: 13, A18, A19;

        then

         A20: ((((p1 `2 ) ^2 ) * D) / D) >= ((((p2 `2 ) ^2 ) * D) / D) by XREAL_1: 72;

        

         A21: ((((p1 `2 ) ^2 ) * D) / D) = ((p1 `2 ) ^2 ) by XCMPLX_1: 89, A1;

        ((((p2 `2 ) ^2 ) * D) / D) = ((p2 `2 ) ^2 ) by XCMPLX_1: 89, A1;

        then

         A22: ( sqrt ((p1 `2 ) ^2 )) >= ( sqrt ((p2 `2 ) ^2 )) by SQUARE_1: 26, A20, A21;

        ( sqrt ((p2 `2 ) ^2 )) = (p2 `2 ) by SQUARE_1: 22, A12;

        then

         A23: (p1 `2 ) >= (p2 `2 ) by A22, SQUARE_1: 22, A11;

        ((p1 `2 ) * ( sqrt D)) >= ((p2 `2 ) * ( sqrt D)) by A23, XREAL_1: 64, A10;

        hence contradiction by A1, A9, XREAL_1: 7;

      end;

    end;

    theorem :: PELLS_EQ:20

    

     Th20: for D be non square Nat, p be positive Pell's_solution of D, a,b be Integer, n be Nat st n > 0 & (a + (b * ( sqrt D))) = (((p `1 ) + ((p `2 ) * ( sqrt D))) |^ n) holds [a, b] is positive Pell's_solution of D

    proof

      let D be non square Nat;

      let p be positive Pell's_solution of D;

      let a,b be Integer, n be Nat such that

       A1: n > 0 and

       A2: (a + (b * ( sqrt D))) = (((p `1 ) + ((p `2 ) * ( sqrt D))) |^ n);

      

       A3: D = (( sqrt D) ^2 ) by SQUARE_1:def 2;

      

      then ((a ^2 ) - ((b ^2 ) * D)) = ((a + (b * ( sqrt D))) * (a - (b * ( sqrt D))))

      .= ((((p `1 ) + ((p `2 ) * ( sqrt D))) |^ n) * (((p `1 ) - ((p `2 ) * ( sqrt D))) |^ n)) by A2, Th6

      .= ((((p `1 ) + ((p `2 ) * ( sqrt D))) * ((p `1 ) - ((p `2 ) * ( sqrt D)))) |^ n) by NEWTON: 7

      .= ((((p `1 ) ^2 ) - (((p `2 ) ^2 ) * D)) |^ n) by A3

      .= (1 |^ n) by Def1

      .= 1;

      then

      reconsider ab = [a, b] as Pell's_solution of D by Lm4;

      ((p `1 ) + ((p `2 ) * ( sqrt D))) > 1 by Th18;

      then ((ab `1 ) + ((ab `2 ) * ( sqrt D))) > (1 |^ n) by A2, NEWTON02: 40, A1;

      hence thesis by Th18;

    end;

    definition

      let D be non square Nat;

      :: PELLS_EQ:def3

      func min_Pell's_solution_of D -> positive Pell's_solution of D means

      : Def3: for p be positive Pell's_solution of D holds (it `1 ) <= (p `1 ) & (it `2 ) <= (p `2 );

      existence

      proof

        defpred M[ Nat] means ex p be positive Pell's_solution of D st (p `1 ) = $1;

        set p = the positive Pell's_solution of D;

        reconsider p1 = (p `1 ) as Element of NAT by INT_1: 3;

         M[p1];

        then

         A1: ex n be Nat st M[n];

        consider m be Nat such that

         A2: M[m] & for n be Nat st M[n] holds m <= n from NAT_1:sch 5( A1);

        consider p be positive Pell's_solution of D such that

         A3: (p `1 ) = m by A2;

        take p;

        let q be positive Pell's_solution of D;

        set pp = ((p `1 ) + ((p `2 ) * ( sqrt D))), qq = ((q `1 ) + ((q `2 ) * ( sqrt D)));

        

         A4: pp > 1 & qq > 1 & (q `1 ) in NAT by Th18, INT_1: 3;

        pp > qq or pp = qq or pp < qq by XXREAL_0: 1;

        hence thesis by A2, A3, A4, Th19, Th3;

      end;

      uniqueness

      proof

        let p1,p2 be positive Pell's_solution of D such that

         A5: for p be positive Pell's_solution of D holds (p1 `1 ) <= (p `1 ) & (p1 `2 ) <= (p `2 ) and

         A6: for p be positive Pell's_solution of D holds (p2 `1 ) <= (p `1 ) & (p2 `2 ) <= (p `2 );

        (p1 `1 ) <= (p2 `1 ) & (p1 `1 ) >= (p2 `1 ) & (p1 `2 ) <= (p2 `2 ) & (p1 `2 ) >= (p2 `2 ) by A5, A6;

        then

         A7: (p1 `1 ) = (p2 `1 ) & (p1 `2 ) = (p2 `2 ) by XXREAL_0: 1;

        p1 = [(p1 `1 ), (p1 `2 )] & p2 = [(p2 `1 ), (p2 `2 )];

        hence thesis by A7;

      end;

    end

    theorem :: PELLS_EQ:21

    for D be non square Nat holds for p be Element of [: INT , INT :] holds p is positive Pell's_solution of D iff ex n be positive Nat st ((p `1 ) + ((p `2 ) * ( sqrt D))) = (((( min_Pell's_solution_of D) `1 ) + ((( min_Pell's_solution_of D) `2 ) * ( sqrt D))) |^ n)

    proof

      let D be non square Nat;

      let p be Element of [: INT , INT :];

      set m = ( min_Pell's_solution_of D), t = (m `1 ), u = (m `2 ), S = ( sqrt D), x = (p `1 ), y = (p `2 );

      

       A1: (S ^2 ) = D by SQUARE_1:def 2;

      thus p is positive Pell's_solution of D implies ex n be positive Nat st (x + (y * S)) = ((t + (u * S)) |^ n)

      proof

        assume

         A2: p is positive Pell's_solution of D;

        assume

         A3: for n be positive Nat holds (x + (y * S)) <> ((t + (u * S)) |^ n);

        ex n st ((t + (u * S)) |^ n) < (x + (y * S)) < ((t + (u * S)) |^ (n + 1)) & n > 0

        proof

          set L = [\(( log (10,(x + (y * S)))) / ( log (10,(t + (u * S)))))/];

          

           A4: (x + (y * S)) > 1 & (t + (u * S)) > 1 by A2, Th18;

          ((t + (u * S)) |^ 1) = (t + (u * S));

          then

           A6: (x + (y * S)) > (t + (u * S)) or (t + (u * S)) > (x + (y * S)) by XXREAL_0: 1, A3;

          x >= t & y >= u by A2, Def3;

          then

           A7: ( log (10,1)) < ( log (10,(t + (u * S)))) < ( log (10,(x + (y * S)))) & ( log (10,1)) = 0 by A2, A4, A6, Th19, POWER: 51, POWER: 57;

          then 1 < (( log (10,(x + (y * S)))) / ( log (10,(t + (u * S))))) by XREAL_1: 187;

          then

           A8: (1 - 1) < ((( log (10,(x + (y * S)))) / ( log (10,(t + (u * S))))) - 1) by XREAL_1: 9;

          ((( log (10,(x + (y * S)))) / ( log (10,(t + (u * S))))) - 1) < L by INT_1:def 6;

          then

          reconsider L as Element of NAT by INT_1: 3, A8;

          take L;

          ((t + (u * S)) |^ L) = ((t + (u * S)) to_power L) by POWER: 41;

          then

           A10: ( log (10,((t + (u * S)) |^ L))) = (L * ( log (10,(t + (u * S))))) by A4, POWER: 55;

          

           A11: 0 < L by A8, INT_1:def 6;

          (L * ( log (10,(t + (u * S))))) <= ( log (10,(x + (y * S)))) by XREAL_1: 83, A7, INT_1:def 6;

          then ((t + (u * S)) |^ L) <= (x + (y * S)) by A4, A10, POWER: 57;

          hence ((t + (u * S)) |^ L) < (x + (y * S)) by A11, A3, XXREAL_0: 1;

          ((t + (u * S)) |^ (L + 1)) = ((t + (u * S)) to_power (L + 1)) by POWER: 41;

          then ( log (10,((t + (u * S)) |^ (L + 1)))) = ((L + 1) * ( log (10,(t + (u * S))))) by A4, POWER: 55;

          then ( log (10,((t + (u * S)) |^ (L + 1)))) > ( log (10,(x + (y * S)))) by INT_1: 29, XREAL_1: 77, A7;

          then ((t + (u * S)) |^ (L + 1)) >= (x + (y * S)) by A4, POWER: 57;

          hence thesis by A3, XXREAL_0: 1, INT_1:def 6, A8;

        end;

        then

        consider n be Nat such that

         A12: ((t + (u * S)) |^ n) < (x + (y * S)) < ((t + (u * S)) |^ (n + 1)) and

         A13: n > 0 ;

        consider tn,un be Nat such that

         A14: ((t + (u * S)) |^ n) = (tn + (un * S)) by Th4;

        reconsider TU = [tn, un] as positive Pell's_solution of D by A14, A13, Th20;

        

         A15: (TU `1 ) = tn & (TU `2 ) = un;

        

         A16: ((tn ^2 ) - ((un ^2 ) * D)) = 1 by A15, Lm4;

        then

         A17: ((tn + (un * S)) * (tn - (un * S))) = 1 by A1;

        (tn + (un * S)) > 1 by A15, Th18;

        then (tn - (un * S)) > 0 by A17;

        then

         A18: (((t + (u * S)) |^ n) * (tn - (un * S))) < ((x + (y * S)) * (tn - (un * S))) < (((t + (u * S)) |^ (n + 1)) * (tn - (un * S))) by A12, XREAL_1: 68;

        

         A19: 1 < ((x + (y * S)) * (tn - (un * S))) < (t + (u * S))

        proof

          (((t + (u * S)) |^ (n + 1)) * (tn - (un * S))) = (((tn + (un * S)) * (t + (u * S))) * (tn - (un * S))) by A14, NEWTON: 6

          .= (((tn + (un * S)) * (tn - (un * S))) * (t + (u * S)))

          .= (t + (u * S)) by A1, A16;

          hence thesis by A18, A16, A1, A14;

        end;

        set a = ((x * tn) - ((y * un) * D)), b = ((y * tn) - (x * un));

        ((a ^2 ) - (D * (b ^2 ))) = ((((x ^2 ) - ((y ^2 ) * D)) * (tn - (un * S))) * (tn + (un * S))) by A1

        .= ((1 * (tn - (un * S))) * (tn + (un * S))) by A2, Def1

        .= 1 by A1, A16;

        then

        reconsider ab = [a, b] as Pell's_solution of D by Lm4;

        ((x + (y * S)) * (tn - (un * S))) = ((ab `1 ) + ((ab `2 ) * S)) by A1;

        then

         A20: ab is positive by A19, Th18;

        1 < ((ab `1 ) + ((ab `2 ) * S)) < (t + (u * S)) by A19, A1;

        then (ab `1 ) < t & (ab `2 ) < u by Th19;

        hence thesis by A20, Def3;

      end;

      assume ex n be positive Nat st (x + (y * S)) = ((t + (u * S)) |^ n);

      then [x, y] is positive Pell's_solution of D by Th20;

      hence thesis;

    end;