let n be Nat; :: thesis: 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; :: thesis: ( 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; :: thesis: verum