let n be Nat; for a being non trivial Nat holds
( Px (a,(n + 1)) = ((Px (a,n)) * a) + ((Py (a,n)) * ((a ^2) -' 1)) & Py (a,(n + 1)) = (Px (a,n)) + ((Py (a,n)) * a) )
let a be non trivial Nat; ( Px (a,(n + 1)) = ((Px (a,n)) * a) + ((Py (a,n)) * ((a ^2) -' 1)) & Py (a,(n + 1)) = (Px (a,n)) + ((Py (a,n)) * a) )
set A = (a ^2) -' 1;
set M = min_Pell's_solution_of ((a ^2) -' 1);
set n1 = n + 1;
A1:
(sqrt ((a ^2) -' 1)) ^2 = (a ^2) -' 1
by SQUARE_1:def 2;
A2:
min_Pell's_solution_of ((a ^2) -' 1) = [a,1]
by Th8;
(Px (a,(n + 1))) + ((Py (a,(n + 1))) * (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 + 1)
by Def2
.=
((((min_Pell's_solution_of ((a ^2) -' 1)) `1) + (((min_Pell's_solution_of ((a ^2) -' 1)) `2) * (sqrt ((a ^2) -' 1)))) |^ n) * (((min_Pell's_solution_of ((a ^2) -' 1)) `1) + (((min_Pell's_solution_of ((a ^2) -' 1)) `2) * (sqrt ((a ^2) -' 1))))
by NEWTON:6
.=
((Px (a,n)) + ((Py (a,n)) * (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))))
by Def2
.=
(((Px (a,n)) * a) + ((Py (a,n)) * ((a ^2) -' 1))) + (((Px (a,n)) + ((Py (a,n)) * a)) * (sqrt ((a ^2) -' 1)))
by A2, A1
;
hence
( Px (a,(n + 1)) = ((Px (a,n)) * a) + ((Py (a,n)) * ((a ^2) -' 1)) & Py (a,(n + 1)) = (Px (a,n)) + ((Py (a,n)) * a) )
by PELLS_EQ:3; verum