let a be Real; :: thesis: for n being Nat st a > - 1 & a <= 0 & n is odd holds
( a >= n -root a & n -root a > - 1 )
let n be Nat; :: thesis: ( a > - 1 & a <= 0 & n is odd implies ( a >= n -root a & n -root a > - 1 ) )
assume that
A1: a > - 1 and
A2: a <= 0 ; :: thesis: ( not n is odd or ( a >= n -root a & n -root a > - 1 ) )
assume n is odd ; :: thesis: ( a >= n -root a & n -root a > - 1 )
then A3: ex m being Nat st n = (2 * m) + 1 by ABIAN:9;
then A4: ( n >= 1 & - a < 1 ) by A1, ABIAN:12, XREAL_1:25;
then A5: n -root (- a) < 1 by A2, Th20;
A6: - a <= n -root (- a) by A2, A4, Th20;
A7: - (n -root (- a)) > - 1 by A5, XREAL_1:24;
a >= - (n -root (- a)) by A6, XREAL_1:26;
hence ( a >= n -root a & n -root a > - 1 ) by A3, A7, Th10; :: thesis: verum