let a, b be Real; :: thesis: for n being Nat st a >= 0 & a < b & n >= 1 holds

n -Root a < n -Root b

let n be Nat; :: thesis: ( a >= 0 & a < b & n >= 1 implies n -Root a < n -Root b )

assume that

A1: a >= 0 and

A2: a < b and

A3: n >= 1 and

A4: n -Root a >= n -Root b ; :: thesis: contradiction

(n -Root a) |^ n = a by A1, A3, Th19;

then A5: (n -Root a) |^ n < (n -Root b) |^ n by A1, A2, A3, Lm2;

n -Root b > 0 by A1, A2, A3, Def2;

hence contradiction by A4, A5, Th9; :: thesis: verum

n -Root a < n -Root b

let n be Nat; :: thesis: ( a >= 0 & a < b & n >= 1 implies n -Root a < n -Root b )

assume that

A1: a >= 0 and

A2: a < b and

A3: n >= 1 and

A4: n -Root a >= n -Root b ; :: thesis: contradiction

(n -Root a) |^ n = a by A1, A3, Th19;

then A5: (n -Root a) |^ n < (n -Root b) |^ n by A1, A2, A3, Lm2;

n -Root b > 0 by A1, A2, A3, Def2;

hence contradiction by A4, A5, Th9; :: thesis: verum