let a, b be real number ; :: thesis: for n being Element of NAT st a < b & ( ( a >= 0 & n >= 1 ) or not n is even ) holds
n -root a < n -root b
let n be Element of NAT ; :: thesis: ( a < b & ( ( a >= 0 & 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:37;
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: - a > 0 by A13, XREAL_1:60;

A15: now

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

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

A17: n -root b >= 0 by A10, A16, Th8;
A18: n -Root (- a) > 0 by A10, A14, PREPOWER:def 3;
A19: - (n -Root (- a)) < - 0 by A18, XREAL_1:26;
thus n -root a < n -root b by A9, A13, A17, A19, Def1; :: thesis: verum

end;

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

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

end;

end;

end;

thus n -root a < n -root b by A15; :: 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