let a be Real; for p being Rational st a >= 1 & p >= 0 holds
a #Q p >= 1
let p be Rational; ( a >= 1 & p >= 0 implies a #Q p >= 1 )
assume that
A1:
a >= 1
and
A2:
p >= 0
; a #Q p >= 1
numerator p >= 0
by A2, RAT_1:37;
then reconsider n = numerator p as Element of NAT by INT_1:3;
A3:
a #Z (numerator p) = a |^ n
by Th36;
a |^ n >= 1 |^ n
by A1, Th9;
then A4:
a #Z (numerator p) >= 1
by A3;
denominator p >= 1
by RAT_1:11;
hence
a #Q p >= 1
by A4, Th29; verum