let a be Real; :: thesis: for n being Nat st a > 0 & n >= 1 holds
(n -Root a) - 1 <= (a - 1) / n
let n be Nat; :: thesis: ( a > 0 & n >= 1 implies (n -Root a) - 1 <= (a - 1) / n )
assume that
A1: a > 0 and
A2: n >= 1 ; :: thesis: (n -Root a) - 1 <= (a - 1) / n
n -Root a > 0 by A1, A2, Def2;
then (n -Root a) - 1 > 0 - 1 by XREAL_1:9;
then (1 + ((n -Root a) - 1)) |^ n >= 1 + (n * ((n -Root a) - 1)) by Th16;
then a >= 1 + (n * ((n -Root a) - 1)) by A1, A2, Lm2;
then a - 1 >= n * ((n -Root a) - 1) by XREAL_1:19;
then (a - 1) / n >= (n * ((n -Root a) - 1)) / n by XREAL_1:72;
hence (n -Root a) - 1 <= (a - 1) / n by A2, XCMPLX_1:89; :: thesis: verum