let a, b be real number ; :: thesis: for n being Element of NAT st a <= b & ( ( 0 <= a & n >= 1 ) or ex m being Element of NAT st n = (2 * m) + 1 ) holds
n -root a <= n -root b
let n be Element of NAT ; :: thesis: ( a <= b & ( ( 0 <= a & n >= 1 ) or ex m being Element of NAT st n = (2 * m) + 1 ) implies n -root a <= n -root b )
assume that
A1: a <= b and
A2: ( ( 0 <= a & n >= 1 ) or ex m being Element of NAT st n = (2 * m) + 1 ) ; :: 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 A4: ( 0 <= a & n >= 1 & a <= b ) ; :: thesis: n -root a <= n -root b
then n -Root a <= n -Root b by PREPOWER:36;
then n -Root a <= n -root b by A4, Def1;
hence n -root a <= n -root b by A4, Def1; :: thesis: verum

end;

now

assume A5: ex m being Element of NAT st n = (2 * m) + 1 ; :: thesis: n -root a <= n -root b
then consider m being Element of NAT such that
A6: n = (2 * m) + 1 ;
A7: n >= 0 + 1 by A6, XREAL_1:8;

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 a < 0 ; :: thesis: n -root a <= n -root b

then A8: - a >= 0 ;

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 A5, A9, Th11; :: thesis: verum

end;

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

then A10: - b >= 0 ;
- a >= - b by A1, XREAL_1:26;
then n -root (- a) >= n -root (- b) by A3, A7, A10;
then - (n -root (- a)) <= - (n -root (- b)) by XREAL_1:26;
then n -root a <= - (n -root (- b)) by A5, Th11;
hence n -root a <= n -root b by A5, 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