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