let a be Real; :: thesis: for n being Nat st 0 <= a & a < 1 & n >= 1 holds
( a <= n -Root a & n -Root a < 1 )
let n be Nat; :: thesis: ( 0 <= a & a < 1 & n >= 1 implies ( a <= n -Root a & n -Root a < 1 ) )
assume that
A1: 0 <= a and
A2: a < 1 and
A3: n >= 1 ; :: thesis: ( a <= n -Root a & n -Root a < 1 )

A4: now :: thesis: a |^ n >= 0

per cases ( a > 0 or a = 0 ) by A1;

suppose a > 0 ; :: thesis: a |^ n >= 0

hence a |^ n >= 0 by Th6; :: thesis: verum

end;

suppose a = 0 ; :: thesis: a |^ n >= 0

hence a |^ n >= 0 ; :: thesis: verum

end;

end;

end;

now :: thesis: a |^ n <= a

per cases ( a > 0 or a = 0 ) by A1;

suppose a > 0 ; :: thesis: a |^ n <= a

hence a |^ n <= a by A2, A3, Th14; :: thesis: verum

end;

suppose a = 0 ; :: thesis: a |^ n <= a

hence a |^ n <= a by A3, NEWTON:11; :: thesis: verum

end;

end;

end;

then n -Root (a |^ n) <= n -Root a by A3, A4, Th27;
hence a <= n -Root a by A1, A3, Th19; :: thesis: n -Root a < 1
n -Root a < n -Root 1 by A1, A2, A3, Th28;
hence n -Root a < 1 by A3, Th20; :: thesis: verum