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