let a be Real; :: thesis: for p being Rational st a > 0 & a < 1 & p > 0 holds

a #Q p < 1

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

reconsider q = 0 as Rational ;

assume that

A1: a > 0 and

A2: a < 1 and

A3: p > 0 ; :: thesis: a #Q p < 1

1 / a > 1 by A1, A2, Lm4, XREAL_1:88;

then (1 / a) #Q p > (1 / a) #Q q by A3, Th64;

then (1 / a) #Q p > 1 by Th47;

then 1 / (a #Q p) > 1 by A1, Th57;

hence a #Q p < 1 by XREAL_1:185; :: thesis: verum

a #Q p < 1

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

reconsider q = 0 as Rational ;

assume that

A1: a > 0 and

A2: a < 1 and

A3: p > 0 ; :: thesis: a #Q p < 1

1 / a > 1 by A1, A2, Lm4, XREAL_1:88;

then (1 / a) #Q p > (1 / a) #Q q by A3, Th64;

then (1 / a) #Q p > 1 by Th47;

then 1 / (a #Q p) > 1 by A1, Th57;

hence a #Q p < 1 by XREAL_1:185; :: thesis: verum