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

( n -Root a >= 1 & a >= n -Root a )

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

assume that

A1: a >= 1 and

A2: n >= 1 ; :: thesis: ( n -Root a >= 1 & a >= n -Root a )

n -Root a >= n -Root 1 by A1, A2, Th27;

hence n -Root a >= 1 by A2, Th20; :: thesis: a >= n -Root a

n -Root a <= n -Root (a |^ n) by A1, A2, Th12, Th27;

hence a >= n -Root a by A1, A2, Lm2; :: thesis: verum

( n -Root a >= 1 & a >= n -Root a )

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

assume that

A1: a >= 1 and

A2: n >= 1 ; :: thesis: ( n -Root a >= 1 & a >= n -Root a )

n -Root a >= n -Root 1 by A1, A2, Th27;

hence n -Root a >= 1 by A2, Th20; :: thesis: a >= n -Root a

n -Root a <= n -Root (a |^ n) by A1, A2, Th12, Th27;

hence a >= n -Root a by A1, A2, Lm2; :: thesis: verum