let n1, n2 be Nat; for a being non trivial Nat st [n1,n2] is Pell's_solution of (a ^2) -' 1 holds
ex n being Nat st
( n1 = Px (a,n) & n2 = Py (a,n) )
let a be non trivial Nat; ( [n1,n2] is Pell's_solution of (a ^2) -' 1 implies ex n being Nat st
( n1 = Px (a,n) & n2 = Py (a,n) ) )
set D = (a ^2) -' 1;
assume A1:
[n1,n2] is Pell's_solution of (a ^2) -' 1
; ex n being Nat st
( n1 = Px (a,n) & n2 = Py (a,n) )
then reconsider N = [n1,n2] as Pell's_solution of (a ^2) -' 1 ;
A2:
(n1 ^2) - (((a ^2) -' 1) * (n2 ^2)) = 1
by A1, Lm3;
per cases
( n2 = 0 or n2 > 0 )
;
suppose
n2 > 0
;
ex n being Nat st
( n1 = Px (a,n) & n2 = Py (a,n) )then
N is
positive
by A2;
then consider n being
positive Nat such that A4:
n1 + (n2 * (sqrt ((a ^2) -' 1))) = (((min_Pell's_solution_of ((a ^2) -' 1)) `1) + (((min_Pell's_solution_of ((a ^2) -' 1)) `2) * (sqrt ((a ^2) -' 1)))) |^ n
by PELLS_EQ:21;
consider y being
Nat such that A5:
(Px (a,n)) + (y * (sqrt ((a ^2) -' 1))) = (((min_Pell's_solution_of ((a ^2) -' 1)) `1) + (((min_Pell's_solution_of ((a ^2) -' 1)) `2) * (sqrt ((a ^2) -' 1)))) |^ n
by Def1;
A6:
n1 = Px (
a,
n)
by A5, A4, PELLS_EQ:3;
(Px (a,n)) + ((Py (a,n)) * (sqrt ((a ^2) -' 1))) = n1 + (n2 * (sqrt ((a ^2) -' 1)))
by A4, Def2;
then
n2 = Py (
a,
n)
by PELLS_EQ:3;
hence
ex
n being
Nat st
(
n1 = Px (
a,
n) &
n2 = Py (
a,
n) )
by A6;
verum end; end;