let a, b be Real; :: thesis: for n being Nat st a < b & ( ( a >= 0 & n >= 1 ) or n is odd ) holds
n -root a < n -root b
let n be Nat; :: thesis: ( a < b & ( ( a >= 0 & n >= 1 ) or n is odd ) implies n -root a < n -root b )
assume that
A1: a < b and
A2: ( ( 0 <= a & n >= 1 ) or n is odd ) ; :: thesis: n -root a < n -root b

A3: now :: thesis: for a, b being Real
for n being Nat st 0 <= a & n >= 1 & a < b holds
n -root a < n -root b

let a, b be Real; :: thesis: for n being Nat st 0 <= a & n >= 1 & a < b holds
n -root a < n -root b
let n be Nat; :: thesis: ( 0 <= a & n >= 1 & a < b implies n -root a < n -root b )
assume that
A4: ( 0 <= a & n >= 1 ) and
A5: a < b ; :: thesis: n -root a < n -root b
n -Root a < n -Root b by A4, A5, PREPOWER:28;
then n -Root a < n -root b by A4, A5, Def1;
hence n -root a < n -root b by A4, Def1; :: thesis: verum

end;

now :: thesis: ( n is odd implies n -root a < n -root b )

assume A6: n is odd ; :: thesis: n -root a < n -root b
then A7: n >= 1 by ABIAN:12;

now :: thesis: n -root a < n -root b

per cases ( a >= 0 or a < 0 ) ;

suppose a >= 0 ; :: thesis: n -root a < n -root b

hence n -root a < n -root b by A1, A3, A7; :: thesis: verum

end;

suppose A8: a < 0 ; :: thesis: n -root a < n -root b

then A9: - a > 0 by XREAL_1:58;

now :: thesis: n -root a < n -root b

per cases ( b >= 0 or b < 0 ) ;

suppose b >= 0 ; :: thesis: n -root a < n -root b

then A10: n -root b >= 0 by A7, Th7;
n -Root (- a) > 0 by A7, A9, PREPOWER:def 2;
then - (n -Root (- a)) < - 0 by XREAL_1:24;
hence n -root a < n -root b by A6, A8, A10, Def1; :: thesis: verum

end;

suppose A11: b < 0 ; :: thesis: n -root a < n -root b

- a > - b by A1, XREAL_1:24;
then n -root (- a) > n -root (- b) by A3, A7, A11;
then - (n -root (- a)) < - (n -root (- b)) by XREAL_1:24;
then n -root a < - (n -root (- b)) by A6, Th10;
hence n -root a < n -root b by A6, Th10; :: thesis: verum

end;

end;

end;

hence n -root a < n -root b ; :: thesis: verum

end;

end;

end;

hence n -root a < n -root b ; :: thesis: verum

end;

hence n -root a < n -root b by A1, A2, A3; :: thesis: verum