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 numerator p >= 0 by RAT_1:76;
then reconsider n = numerator p as Element of NAT by INT_1:16;
A2: denominator p >= 1 by RAT_1:29;
A3: a #Z (numerator p) = a |^ n by Th46;
a |^ n >= 1 |^ n by A1, Th17;
then a #Z (numerator p) >= 1 by A3, NEWTON:15;
hence a #Q p >= 1 by A2, Th38; :: thesis: verum