let a, b, c be real number ; :: thesis: ( a < b & c > 1 implies c to_power a < c to_power b )
assume that
A1: a < b and
A2: c > 1 ; :: thesis: c to_power a < c to_power b
A3: c to_power a > 0 by A2, Th39;
A4: c to_power a <> 0 by A2, Th39;
A5: b - a > 0 by A1, XREAL_1:52;
A6: c to_power (b - a) > 1 by A2, A5, Th40;
A7: (c to_power b) / (c to_power a) > 1 by A2, A6, Th34;
A8: ((c to_power b) / (c to_power a)) * (c to_power a) > 1 * (c to_power a) by A3, A7, XREAL_1:70;
thus c to_power a < c to_power b by A4, A8, XCMPLX_1:88; :: thesis: verum