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

(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