let a be real number ; :: thesis: for n being Element of NAT st a > - 1 & a <= 0 & ex m being Element of NAT st n = (2 * m) + 1 holds
( a >= n -root a & n -root a > - 1 )
let n be Element of NAT ; :: thesis: ( a > - 1 & a <= 0 & ex m being Element of NAT st n = (2 * m) + 1 implies ( a >= n -root a & n -root a > - 1 ) )
assume A1: ( a > - 1 & a <= 0 & ex m being Element of NAT st n = (2 * m) + 1 ) ; :: thesis: ( a >= n -root a & n -root a > - 1 )
then consider m being Element of NAT such that
A2: n = (2 * m) + 1 ;
A3: n >= 0 + 1 by A2, XREAL_1:8;
A4: - a < 1 by A1, XREAL_1:27;
- a >= - 0 by A1;
then ( n -root (- a) < 1 & - a <= n -root (- a) ) by A3, A4, Th21;
then ( - (n -root (- a)) > - 1 & a >= - (n -root (- a)) ) by XREAL_1:26, XREAL_1:28;
hence ( a >= n -root a & n -root a > - 1 ) by A1, Th11; :: thesis: verum