let a be Real; :: 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 that

A1: a >= 1 and

A2: p >= 0 ; :: thesis: 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; :: thesis: verum

a #Q p >= 1

let p be Rational; :: thesis: ( a >= 1 & p >= 0 implies a #Q p >= 1 )

assume that

A1: a >= 1 and

A2: p >= 0 ; :: thesis: 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; :: thesis: verum