theorem :: NEWTON02:43

for n, a being Nat ex b being Nat st
( b |^ (n + 1) <= a & a < (b + 1) |^ (n + 1) )