let a be real number ; :: thesis: for n being Element of NAT st 0 <= a & a < 1 & n >= 1 holds
( a <= n -Root a & n -Root a < 1 )
let n be Element of NAT ; :: thesis: ( 0 <= a & a < 1 & n >= 1 implies ( a <= n -Root a & n -Root a < 1 ) )
assume that
A1: ( 0 <= a & a < 1 ) and
A2: n >= 1 ; :: thesis: ( a <= n -Root a & n -Root a < 1 )

A3: now

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

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

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

end;

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

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

end;

end;

end;

now

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

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

hence a |^ n <= a by A1, A2, Th22; :: thesis: verum

end;

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

hence a |^ n <= a by A2, NEWTON:16; :: thesis: verum

end;

end;

end;

then n -Root (a |^ n) <= n -Root a by A2, A3, Th36;
hence a <= n -Root a by A1, A2, Th28; :: thesis: n -Root a < 1
n -Root a < n -Root 1 by A1, A2, Th37;
hence n -Root a < 1 by A2, Th29; :: thesis: verum