let a, b be real number ; :: thesis: for n being Element of NAT st a <= b & ( ( 0 <= a & n >= 1 ) or not n is even ) holds
n -root a <= n -root b
let n be Element of NAT ; :: thesis: ( a <= b & ( ( 0 <= a & n >= 1 ) or not n is even ) implies n -root a <= n -root b )
assume that
A1: a <= b and
A2: ( ( 0 <= a & n >= 1 ) or not n is even ) ; :: thesis: n -root a <= n -root b

A3: now

let a, b be real number ; :: thesis: for n being Element of NAT st 0 <= a & n >= 1 & a <= b holds
n -root a <= n -root b
let n be Element of 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

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

now

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

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