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 )

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

( 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 )

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