let a be real number ; :: thesis: for n being Element of NAT st a > 0 & n >= 1 holds
(n -root a) - 1 <= (a - 1) / n
let n be Element of NAT ; :: thesis: ( a > 0 & n >= 1 implies (n -root a) - 1 <= (a - 1) / n )
assume A1: ( a > 0 & n >= 1 ) ; :: thesis: (n -root a) - 1 <= (a - 1) / n
A2: (n -Root a) - 1 <= (a - 1) / n by A1, PREPOWER:40;
thus (n -root a) - 1 <= (a - 1) / n by A1, A2, Def1; :: thesis: verum