let a be real number ; :: thesis: for n being Element of NAT st a <= - 1 & not n is even holds
( n -root a <= - 1 & a <= n -root a )
let n be Element of NAT ; :: thesis: ( a <= - 1 & not n is even implies ( n -root a <= - 1 & a <= n -root a ) )
assume that
A1: a <= - 1 and
A2: not n is even ; :: thesis: ( n -root a <= - 1 & a <= n -root a )
A3: ( n >= 1 & - a >= 1 ) by A1, A2, ABIAN:12, XREAL_1:27;
then A4: n -root (- a) >= 1 by Th19;
A5: - a >= n -root (- a) by A3, Th19;
A6: - (n -root (- a)) <= - 1 by A4, XREAL_1:26;
a <= - (n -root (- a)) by A5, XREAL_1:27;
hence ( n -root a <= - 1 & a <= n -root a ) by A2, A6, Th11; :: thesis: verum