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

a #Q p > a #Q q

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

assume that

A1: a > 1 and

A2: p > q ; :: thesis: a #Q p > a #Q q

A3: p - q > 0 by A2, XREAL_1:50;

A4: (a #Q p) / (a #Q q) = a #Q (p - q) by A1, Th55;

A5: a #Q q <> 0 by A1, Th52;

a #Q q > 0 by A1, Th52;

then ((a #Q p) / (a #Q q)) * (a #Q q) > 1 * (a #Q q) by A1, A3, A4, Th62, XREAL_1:68;

hence a #Q p > a #Q q by A5, XCMPLX_1:87; :: thesis: verum

a #Q p > a #Q q

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

assume that

A1: a > 1 and

A2: p > q ; :: thesis: a #Q p > a #Q q

A3: p - q > 0 by A2, XREAL_1:50;

A4: (a #Q p) / (a #Q q) = a #Q (p - q) by A1, Th55;

A5: a #Q q <> 0 by A1, Th52;

a #Q q > 0 by A1, Th52;

then ((a #Q p) / (a #Q q)) * (a #Q q) > 1 * (a #Q q) by A1, A3, A4, Th62, XREAL_1:68;

hence a #Q p > a #Q q by A5, XCMPLX_1:87; :: thesis: verum