:: deftheorem Def2 defines Py HILB10_1:def 2 :
for a, n being Nat st not a is trivial holds
for b₃ being Nat holds
( b₃ = Py (a,n) iff for b being non trivial Nat st b = a holds
(Px (b,n)) + (b₃ * (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 );