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