:: by Marcin Acewicz and Karol P\kak

::

:: Received August 30, 2017

:: Copyright (c) 2017 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 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 )

for a, b, c, d being Integer st a + (b * (sqrt D)) = c + (d * (sqrt D)) holds

( a = c & b = d )

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

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

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 ) )

( 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 )

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 )

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))

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 )

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

{ [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.| ) )

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 )

ex x, y being Nat st

( (x ^2) - (D * (y ^2)) = 1 & y <> 0 )

proof end;

definition

let D be Nat;

ex b_{1} being Element of [:INT,INT:] st ((b_{1} `1) ^2) - (D * ((b_{1} `2) ^2)) = 1

end;
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 ((it `1) ^2) - (D * ((it `2) ^2)) = 1;

ex b

proof end;

:: deftheorem Def1 defines Pell's_solution PELLS_EQ:def 1 :

for D being Nat

for b_{2} being Element of [:INT,INT:] holds

( b_{2} is Pell's_solution of D iff ((b_{2} `1) ^2) - (D * ((b_{2} `2) ^2)) = 1 );

for D being Nat

for b

( b

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;

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

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

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

coherence

for b_{1} being Integer st b_{1} = p `1 holds

b_{1} is positive
by Def2;

coherence

for b_{1} being Integer st b_{1} = p `2 holds

b_{1} is positive
by Def2;

end;
coherence

for b

b

coherence

for b

b

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

for p being positive Element of [:INT,INT:] st D > 0 holds

not p is Pell's_solution of D

proof end;

registration

let D be non square Nat;

existence

ex b_{1} being Pell's_solution of D st b_{1} is positive
by Th16;

end;
existence

ex b

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 )

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 )

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

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;

ex b_{1} being positive Pell's_solution of D st

for p being positive Pell's_solution of D holds

( b_{1} `1 <= p `1 & b_{1} `2 <= p `2 )

for b_{1}, b_{2} being positive Pell's_solution of D st ( for p being positive Pell's_solution of D holds

( b_{1} `1 <= p `1 & b_{1} `2 <= p `2 ) ) & ( for p being positive Pell's_solution of D holds

( b_{2} `1 <= p `1 & b_{2} `2 <= p `2 ) ) holds

b_{1} = b_{2}

end;
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 for p being positive Pell's_solution of D holds

( it `1 <= p `1 & it `2 <= p `2 );

ex b

for p being positive Pell's_solution of D holds

( b

proof end;

uniqueness for b

( b

( b

b

proof end;

:: deftheorem Def3 defines min_Pell's_solution_of PELLS_EQ:def 3 :

for D being non square Nat

for b_{2} being positive Pell's_solution of D holds

( b_{2} = min_Pell's_solution_of D iff for p being positive Pell's_solution of D holds

( b_{2} `1 <= p `1 & b_{2} `2 <= p `2 ) );

for D being non square Nat

for b

( b

( b

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 )

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;