let a be real number ; :: thesis: for n being Element of NAT st a > - 1 & a <= 0 & not n is even holds
( a >= n -root a & n -root a > - 1 )
let n be Element of NAT ; :: thesis: ( a > - 1 & a <= 0 & not n is even implies ( a >= n -root a & n -root a > - 1 ) )
assume that
A1: a > - 1 and
A2: a <= 0 ; :: thesis: ( n is even or ( a >= n -root a & n -root a > - 1 ) )
assume not n is even ; :: thesis: ( a >= n -root a & n -root a > - 1 )
then A3: ex m being Element of NAT st n = (2 * m) + 1 by ABIAN:9;
A4: ( n >= 1 & - a < 1 ) by A1, A3, XREAL_1:27, Lm1;
A5: n -root (- a) < 1 by A2, A4, Th21;
A6: - a <= n -root (- a) by A2, A4, Th21;
A7: - (n -root (- a)) > - 1 by A5, XREAL_1:26;
A8: a >= - (n -root (- a)) by A6, XREAL_1:28;
thus ( a >= n -root a & n -root a > - 1 ) by A3, A7, A8, Th11; :: thesis: verum