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

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

now

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, Th8;
n -Root (- a) > 0 by A7, A9, PREPOWER:def 3;
then - (n -Root (- a)) < - 0 by XREAL_1:26;
hence n -root a < n -root b by A5, A8, A10, Def1; :: thesis: verum

end;

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

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