let D be non square Nat; 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; 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; 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; ( 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
; [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; verum