:: The Pell's Equation
:: by Marcin Acewicz and Karol P\kak
::
:: Received August 30, 2017
:: Copyright (c) 2017-2026 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, FOMODEL0,
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: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;
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: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 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 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 being 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,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 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;
|. 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
::$L https://en.wikipedia.org/wiki/Pell's_equation 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
::$L https://en.wikipedia.org/wiki/Pell's_equation Pell's equation
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) & log(10,1)=0
by A2,A4,A6,Th19,POWER:51,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;