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 that
A1: a <= - 1 and
A2: ex m being Element of NAT st n = (2 * m) + 1 ; :: thesis: ( n -root a <= - 1 & a <= n -root a )
A3: ( n >= 0 + 1 & - a >= 1 ) by A1, A2, XREAL_1:8, XREAL_1:27;
A4: n -root (- a) >= 1 by A3, Th19;
A5: - a >= n -root (- a) by A3, Th19;
A6: - (n -root (- a)) <= - 1 by A4, XREAL_1:26;
A7: a <= - (n -root (- a)) by A5, XREAL_1:27;
thus ( n -root a <= - 1 & a <= n -root a ) by A2, A6, A7, Th11; :: thesis: verum