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
A6: n -Root a <= n -Root b by A4, A5, PREPOWER:36;
A7: n -Root a <= n -root b by A4, A5, A6, Def1;
thus n -root a <= n -root b by A4, A7, Def1; :: thesis: verum

end;

A8: now

assume A9: not n is even ; :: thesis: n -root a <= n -root b
then A10: n >= 1 by Lm1;

A11: now

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

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

thus n -root a <= n -root b by A1, A3, A10, A12; :: thesis: verum

end;

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

A14: now

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

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

A16: n -root b >= 0 by A10, A15, Th8;
A17: n -root (- a) >= 0 by A10, A13, Th8;
A18: - (n -root (- a)) <= - 0 by A17;
thus n -root a <= n -root b by A9, A16, A18, Th11; :: thesis: verum

end;

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

A20: - a >= - b by A1, XREAL_1:26;
A21: n -root (- a) >= n -root (- b) by A3, A10, A19, A20;
A22: - (n -root (- a)) <= - (n -root (- b)) by A21, XREAL_1:26;
A23: n -root a <= - (n -root (- b)) by A9, A22, Th11;
thus n -root a <= n -root b by A9, A23, Th11; :: thesis: verum

end;

end;

end;

thus n -root a <= n -root b by A14; :: thesis: verum

end;

end;

end;

thus n -root a <= n -root b by A11; :: thesis: verum

end;

thus n -root a <= n -root b by A1, A2, A3, A8; :: thesis: verum