let a be real number ; :: thesis: for p being Rational st a > 1 & p > 0 holds
a #Q p > 1
let p be Rational; :: thesis: ( a > 1 & p > 0 implies a #Q p > 1 )
assume A1: ( a > 1 & p > 0 ) ; :: thesis: a #Q p > 1
then A2: numerator p > 0 by RAT_1:77;
then reconsider n = numerator p as Element of NAT by INT_1:16;
A3: a #Z (numerator p) = a |^ n by Th46;
n >= 0 + 1 by A2, NAT_1:13;
then a |^ n > 1 |^ n by A1, Lm1;
then ( a #Z (numerator p) > 1 & 1 >= 0 ) by A3, NEWTON:15;
then (denominator p) -Root (a #Z (numerator p)) > (denominator p) -Root 1 by Th37, RAT_1:29;
hence a #Q p > 1 by Th29, RAT_1:29; :: thesis: verum