let a, b be Real; :: thesis: for n being Nat st a <= b & ( ( 0 <= a & n >= 1 ) or n is odd ) holds
n -root a <= n -root b
let n be Nat; :: thesis: ( a <= b & ( ( 0 <= a & 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:27;
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

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 A9: n -root b >= 0 by A7, Th7;
n -root (- a) >= 0 by A7, A8, Th7;
then - (n -root (- a)) <= - 0 ;
hence n -root a <= n -root b by A6, A9, Th10; :: thesis: verum

end;

suppose A10: 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, A10;
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