:: The Pell's Equation
:: by Marcin Acewicz and Karol P\kak
::
:: Received August 30, 2017
:: Copyright (c) 2017-2021 Association of Mizar Users


Lm1: for r being Real holds
( 0 < ([\r/] - r) + 1 & ([\r/] - r) + 1 <= 1 )

proof end;

Lm2: for a, b being Real st a = - b holds
|.a.| = |.b.|

proof end;

Lm3: for r being Real st r > 0 holds
ex n being Nat st
( 1 / n < r & n > 1 )

proof end;

theorem Th1: :: PELLS_EQ:1
for i, j being Integer st j < 0 holds
( j < i mod j & i mod j <= 0 )
proof end;

theorem Th2: :: PELLS_EQ:2
for i, j being Integer st j <> 0 holds
|.(i mod j).| < |.j.|
proof end;

theorem Th3: :: PELLS_EQ:3
for D being non square Nat
for a, b, c, d being Integer st a + (b * (sqrt D)) = c + (d * (sqrt D)) holds
( a = c & b = d )
proof end;

theorem Th4: :: PELLS_EQ:4
for D, c, d, n being Nat ex a, b being Nat st a + (b * (sqrt D)) = (c + (d * (sqrt D))) |^ n
proof end;

theorem Th5: :: PELLS_EQ:5
for D being Nat
for c, d being Integer
for n being Nat ex a, b being Integer st a + (b * (sqrt D)) = (c + (d * (sqrt D))) |^ n
proof end;

theorem Th6: :: PELLS_EQ:6
for D being non square Nat
for a, b, c, d being Integer
for n being Nat st a + (b * (sqrt D)) = (c + (d * (sqrt D))) |^ n holds
a - (b * (sqrt D)) = (c - (d * (sqrt D))) |^ n
proof end;

theorem Th7: :: PELLS_EQ:7
for n, D being Nat ex F being FinSequence of NAT st
( len F = n + 1 & ( for k being Nat st k in dom F holds
F . k = [\((k - 1) * (sqrt D))/] + 1 ) & ( not D is square implies F is one-to-one ) )
proof end;

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

theorem Th9: :: PELLS_EQ:9
for n, D being Nat st not D is square & n > 1 holds
ex x, y being Integer st
( y <> 0 & |.y.| <= n & 0 < x - (y * (sqrt D)) & x - (y * (sqrt D)) < 1 / n )
proof end;

theorem Th10: :: PELLS_EQ:10
for n, D being Nat
for x, y being Integer st not D is square & n <> 0 & |.y.| <= n & 0 < x - (y * (sqrt D)) & x - (y * (sqrt D)) < 1 / n holds
|.((x ^2) - (D * (y ^2))).| <= (2 * (sqrt D)) + (1 / (n ^2))
proof end;

theorem Th11: :: PELLS_EQ:11
for D being Nat st not D is square holds
ex x, y being Integer st
( y <> 0 & 0 < x - (y * (sqrt D)) & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 )
proof end;

theorem Th12: :: PELLS_EQ:12
for D being Nat st not D is square holds
{ [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 end;

theorem Th13: :: PELLS_EQ:13
for D being Nat st not D is square holds
ex k, a, b, c, d being Integer st
( 0 <> k & (a ^2) - (D * (b ^2)) = k & k = (c ^2) - (D * (d ^2)) & a,c are_congruent_mod k & b,d are_congruent_mod k & ( |.a.| <> |.c.| or |.b.| <> |.d.| ) )
proof end;

:: WP: #39 Solutions to Pell's Equation
theorem Th14: :: PELLS_EQ:14
for D being Nat st not D is square holds
ex x, y being Nat st
( (x ^2) - (D * (y ^2)) = 1 & y <> 0 )
proof end;

definition
let D be Nat;
mode Pell's_solution of D -> Element of [:INT,INT:] means :Def1: :: PELLS_EQ:def 1
((it `1) ^2) - (D * ((it `2) ^2)) = 1;
existence
ex b1 being Element of [:INT,INT:] st ((b1 `1) ^2) - (D * ((b1 `2) ^2)) = 1
proof end;
end;

:: deftheorem Def1 defines Pell's_solution PELLS_EQ:def 1 :
for D being Nat
for b2 being Element of [:INT,INT:] holds
( b2 is Pell's_solution of D iff ((b2 `1) ^2) - (D * ((b2 `2) ^2)) = 1 );

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

proof end;

definition
let D1, D2 be non empty real-membered set ;
let p be Element of [:D1,D2:];
attr p is positive means :Def2: :: PELLS_EQ:def 2
( p `1 is positive & p `2 is positive );
end;

:: deftheorem Def2 defines positive PELLS_EQ:def 2 :
for D1, D2 being non empty real-membered set
for p being Element of [:D1,D2:] holds
( p is positive iff ( p `1 is positive & p `2 is positive ) );

registration
cluster V12() positive for Element of [:INT,INT:];
existence
ex b1 being Element of [:INT,INT:] st b1 is positive
proof end;
end;

registration
let p be positive Element of [:INT,INT:];
cluster p `1 -> positive for Integer;
coherence
for b1 being Integer st b1 = p `1 holds
b1 is positive
by Def2;
cluster p `2 -> positive for Integer;
coherence
for b1 being Integer st b1 = p `2 holds
b1 is positive
by Def2;
end;

theorem :: PELLS_EQ:15
for D being square Nat
for p being positive Element of [:INT,INT:] st D > 0 holds
not p is Pell's_solution of D
proof end;

theorem Th16: :: PELLS_EQ:16
for D being Nat st not D is square holds
ex p being Pell's_solution of D st p is positive
proof end;

registration
let D be non square Nat;
cluster V12() positive for Pell's_solution of D;
existence
ex b1 being Pell's_solution of D st b1 is positive
by Th16;
end;

:: WP: The Cardinality of the Pell's Solutions
theorem :: PELLS_EQ:17
for D being non square Nat holds { ab where ab is positive Pell's_solution of D : verum } is infinite
proof end;

theorem Th18: :: PELLS_EQ:18
for D being Nat
for p being Pell's_solution of D st not D is square holds
( p is positive iff (p `1) + ((p `2) * (sqrt D)) > 1 )
proof end;

theorem Th19: :: PELLS_EQ:19
for D being Nat
for p1, p2 being Pell's_solution of D st 1 < (p1 `1) + ((p1 `2) * (sqrt D)) & (p1 `1) + ((p1 `2) * (sqrt D)) < (p2 `1) + ((p2 `2) * (sqrt D)) & not D is square holds
( p1 `1 < p2 `1 & p1 `2 < p2 `2 )
proof end;

theorem Th20: :: PELLS_EQ:20
for D being non square Nat
for p being positive Pell's_solution of D
for a, b being Integer
for n being 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 end;

definition
let D be non square Nat;
func min_Pell's_solution_of D -> positive Pell's_solution of D means :Def3: :: PELLS_EQ:def 3
for p being positive Pell's_solution of D holds
( it `1 <= p `1 & it `2 <= p `2 );
existence
ex b1 being positive Pell's_solution of D st
for p being positive Pell's_solution of D holds
( b1 `1 <= p `1 & b1 `2 <= p `2 )
proof end;
uniqueness
for b1, b2 being positive Pell's_solution of D st ( for p being positive Pell's_solution of D holds
( b1 `1 <= p `1 & b1 `2 <= p `2 ) ) & ( for p being positive Pell's_solution of D holds
( b2 `1 <= p `1 & b2 `2 <= p `2 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines min_Pell's_solution_of PELLS_EQ:def 3 :
for D being non square Nat
for b2 being positive Pell's_solution of D holds
( b2 = min_Pell's_solution_of D iff for p being positive Pell's_solution of D holds
( b2 `1 <= p `1 & b2 `2 <= p `2 ) );

theorem :: PELLS_EQ:21
for D being non square Nat
for p being Element of [:INT,INT:] holds
( p is positive Pell's_solution of D iff ex n being 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 end;