let D be non square Nat; :: thesis: 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
let p be positive Pell's_solution of D; :: thesis: 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
let a, b be Integer; :: thesis: 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
let n be Nat; :: thesis: ( n > 0 & a + (b * (sqrt D)) = ((p `1) + ((p `2) * (sqrt D))) |^ n implies [a,b] is positive Pell's_solution of D )
assume that
A1: n > 0 and
A2: a + (b * (sqrt D)) = ((p `1) + ((p `2) * (sqrt D))) |^ n ; :: thesis: [a,b] is positive Pell's_solution of D
A3: D = (sqrt D) ^2 by SQUARE_1:def 2;
then (a ^2) - ((b ^2) * D) = (a + (b * (sqrt D))) * (a - (b * (sqrt D)))
.= (((p `1) + ((p `2) * (sqrt D))) |^ n) * (((p `1) - ((p `2) * (sqrt D))) |^ n) by A2, Th6
.= (((p `1) + ((p `2) * (sqrt D))) * ((p `1) - ((p `2) * (sqrt D)))) |^ n by NEWTON:7
.= (((p `1) ^2) - (((p `2) ^2) * D)) |^ n by A3
.= 1 |^ n by Def1
.= 1 ;
then reconsider ab = [a,b] as Pell's_solution of D by Lm4;
(p `1) + ((p `2) * (sqrt D)) > 1 by Th18;
then (ab `1) + ((ab `2) * (sqrt D)) > 1 |^ n by A2, NEWTON02:40, A1;
hence [a,b] is positive Pell's_solution of D by Th18; :: thesis: verum