theorem Th5: :: PELLS_EQ:5
for D being Nat
for c, d being Integer
for n being Nat ex a, b being Integer st a + (b * (sqrt D)) = (c + (d * (sqrt D))) |^ n