theorem Th13: :: HILB10_8:13

for a being non trivial Nat
for s, n, r being Nat st s > 0 & r > 0 & (((s ^2) * (r ^2)) - ((((s ^2) - 1) * (Py (a,(n + 1)))) * r)) - 1, 0 are_congruent_mod (((2 * a) * s) - (s ^2)) - 1 & s * (((s |^ n) ^2) * (s |^ n)) < a & s * ((r ^2) * r) < a holds
r = s |^ n