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

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

per cases
( p = q or p > q )
by A2, XXREAL_0:1;

end;

suppose
p > q
; :: thesis: a #Q p >= a #Q q

then A3:
p - q >= 0
by XREAL_1:50;

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

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

a #Q q >= 0 by A1, Th52;

then ((a #Q p) / (a #Q q)) * (a #Q q) >= 1 * (a #Q q) by A1, A3, A5, Th60, XREAL_1:64;

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

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

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

a #Q q >= 0 by A1, Th52;

then ((a #Q p) / (a #Q q)) * (a #Q q) >= 1 * (a #Q q) by A1, A3, A5, Th60, XREAL_1:64;

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