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 )

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:85;

then (1 / a) #Q p <= 1 by A3, Th61;

then A4: 1 / (a #Q p) <= 1 by A1, Th57;

a #Q p > 0 by A1, Th52;

hence a #Q p >= 1 by A4, XREAL_1:187; :: thesis: verum

a #Q p >= 1

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

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:85;

then (1 / a) #Q p <= 1 by A3, Th61;

then A4: 1 / (a #Q p) <= 1 by A1, Th57;

a #Q p > 0 by A1, Th52;

hence a #Q p >= 1 by A4, XREAL_1:187; :: thesis: verum