:: The Pell's Equation :: by Marcin Acewicz and Karol P\kak :: :: Received August 30, 2017 :: Copyright (c) 2017-2019 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, XXREAL_0, SUBSET_1, TARSKI, ARYTM_3, RELAT_1, ARYTM_1, CARD_1, SQUARE_1, REAL_1, PYTHTRIP, XXREAL_1, FUNCT_1, XBOOLE_0, ZFMISC_1, MCART_1, ORDINAL2, FINSET_1, NAT_1, INT_1, MEMBERED, COMPLEX1, FINSEQ_1, NEWTON, POWER, PELLS_EQ; notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0, XXREAL_1, SQUARE_1, INT_1, MEMBERED, RELAT_1, CARD_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, DOMAIN_1, PYTHTRIP, XXREAL_2, FINSEQ_1, ABSVALUE, NEWTON, POWER; constructors XXREAL_1, RELSET_1, DOMAIN_1, PEPIN, VALUED_1, PYTHTRIP, XXREAL_2, NEWTON, POWER; registrations NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, XXREAL_1, ORDINAL1, SQUARE_1, FINSET_1, FUNCT_2, RELAT_1, FUNCT_1, RELSET_1, XTUPLE_0, NAT_1, MEMBERED, MCART_1, NEWTON03, INT_1, NEWTON, PYTHTRIP, VALUED_0, XXREAL_2; requirements NUMERALS, SUBSET, BOOLE, ARITHM, REAL; definitions TARSKI, FUNCT_1; equalities ORDINAL1, SQUARE_1; expansions TARSKI; theorems TARSKI, ENUMSET1, FUNCT_1, FUNCT_2, CARD_1, NAT_1, ZFMISC_1, RELAT_1, XBOOLE_0, XREAL_1, XXREAL_0, CARD_2, NEWTON, XTUPLE_0, PYTHTRIP, INT_1, FINSEQ_3, FINSEQ_1, NEWTON03, SQUARE_1, XCMPLX_1, XXREAL_1, ABSVALUE, COMPLEX1, XREAL_0, XXREAL_2, FRECHET, WAYBEL26, NEWTON02, POWER; schemes NAT_1, FINSEQ_1, CLASSES1, XXREAL_2; begin :: Preliminaries 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 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 Th2: for i,j be Integer st j <> 0 holds |. i mod j .| < |.j.| proof let x,j be Integer; assume j<>0; then per cases; suppose j > 0; then 0 <= x mod j < j & |.j.|= j by INT_1:57,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 Th3: for D be non square Nat 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 Th4: for c,d,n be Nat 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 Th5: for c,d be Integer, n be Nat 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 Th6: for D be non square Nat 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 :: Solutions to Pell's Equation -- Construction theorem 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,27; per cases by A7,XXREAL_0:1; suppose A10: 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 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.] 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 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 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 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 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 Th12: D is non square implies {[x,y] where x, y is 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 is 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 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 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 is Integer, y is 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 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 is 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 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 is 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 :: Pell's Equation ::$N #39 Solutions to Pell's Equation theorem 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,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; 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:]; 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 for Integer; coherence by Def2; cluster p`2 -> positive for Integer; coherence by Def2; end; theorem 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 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; ::$N The Cardinality of the Pell's Solutions theorem for D be non square Nat holds the set of all ab where ab is positive Pell's_solution of D is infinite proof let D be non square Nat; set P=the set of all ab where ab is 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 :: Solutions to Pell's Equation -- Shape reserve p,p1,p2 for Pell's_solution of D; theorem 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 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 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; 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 for D be non square Nat 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) 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;