theorem Th20: :: PELLS_EQ:20

for D being 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