let a, b be real number ; :: thesis: for n being Element of NAT st a >= 0 & a < b & n >= 1 holds
n -Root a < n -Root b
let n be Element of NAT ; :: thesis: ( a >= 0 & a < b & n >= 1 implies n -Root a < n -Root b )
assume that
A1: ( a >= 0 & a < b & n >= 1 ) and
A2: n -Root a >= n -Root b ; :: thesis: contradiction
(n -Root a) |^ n = a by A1, Th28;
then A3: (n -Root a) |^ n < (n -Root b) |^ n by A1, Lm2;
n -Root b > 0 by A1, Def3;
hence contradiction by A2, A3, Th17; :: thesis: verum