:: deftheorem Def1 defines Px HILB10_1:def 1 :
for a, n being Nat st not a is trivial holds
for b₃ being Nat holds
( b₃ = Px (a,n) iff for b being non trivial Nat st b = a holds
ex y being Nat st b₃ + (y * (sqrt ((b ^2) -' 1))) = (((min_Pell's_solution_of ((b ^2) -' 1)) `1) + (((min_Pell's_solution_of ((b ^2) -' 1)) `2) * (sqrt ((b ^2) -' 1)))) |^ n );