let a be Real; :: thesis: for n being Nat st a <= - 1 & n is odd holds
( n -root a <= - 1 & a <= n -root a )
let n be Nat; :: thesis: ( a <= - 1 & n is odd implies ( n -root a <= - 1 & a <= n -root a ) )
assume that
A1: a <= - 1 and
A2: n is odd ; :: thesis: ( n -root a <= - 1 & a <= n -root a )
A3: ( n >= 1 & - a >= 1 ) by A1, A2, ABIAN:12, XREAL_1:25;
then A4: n -root (- a) >= 1 by Th18;
A5: - a >= n -root (- a) by A3, Th18;
A6: - (n -root (- a)) <= - 1 by A4, XREAL_1:24;
a <= - (n -root (- a)) by A5, XREAL_1:25;
hence ( n -root a <= - 1 & a <= n -root a ) by A2, A6, Th10; :: thesis: verum