:: 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;

:: #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 b₁ being Element of [:INT,INT:] st ((b₁ `1) ^2) - (D * ((b<sub>1</sub> `2) ^2)) = 1

proof end;

end;

:: deftheorem Def1 defines Pell's_solution PELLS_EQ:def 1 :
for D being Nat
for b₂ being Element of [:INT,INT:] holds
( b₂ is Pell's_solution of D iff ((b₂ `1) ^2) - (D * ((b<sub>2</sub> `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 b₁ being Element of [:INT,INT:] st b₁ is positive

proof end;

end;

registration

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

cluster p `1 -> positive for Integer;

coherence
for b₁ being Integer st b₁ = p `1 holds
b₁ is positive by Def2;

cluster p `2 -> positive for Integer;

coherence
for b₁ being Integer st b₁ = p `2 holds
b₁ 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 b₁ being Pell's_solution of D st b₁ is positive by Th16;

end;

:: 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 b₁ being positive Pell's_solution of D st
for p being positive Pell's_solution of D holds
( b₁ `1 <= p `1 & b₁ `2 <= p `2 )

proof end;

uniqueness
for b₁, b₂ being positive Pell's_solution of D st ( for p being positive Pell's_solution of D holds
( b₁ `1 <= p `1 & b₁ `2 <= p `2 ) ) & ( for p being positive Pell's_solution of D holds
( b₂ `1 <= p `1 & b₂ `2 <= p `2 ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines min_Pell's_solution_of PELLS_EQ:def 3 :
for D being non square Nat
for b₂ being positive Pell's_solution of D holds
( b₂ = min_Pell's_solution_of D iff for p being positive Pell's_solution of D holds
( b₂ `1 <= p `1 & b₂ `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;