let a, b, c be Real; :: thesis: ( a < b & c > 0 & c < 1 implies c to_power a > c to_power b )
assume that
A1: a < b and
A2: c > 0 and
A3: c < 1 ; :: thesis: c to_power a > c to_power b
A4: (1 / c) to_power a > 0 by A2, Th34;
A5: (1 / c) to_power a <> 0 by A2, Th34;
A6: c to_power a > 0 by A2, Th34;
c / c < 1 / c by A2, A3, XREAL_1:74;
then A7: 1 < 1 / c by A2, XCMPLX_1:60;
b - a > 0 by A1, XREAL_1:50;
then (1 / c) to_power (b - a) > 1 by A7, Th35;
then ((1 / c) to_power b) / ((1 / c) to_power a) > 1 by A2, Th29;
then (((1 / c) to_power b) / ((1 / c) to_power a)) * ((1 / c) to_power a) > 1 * ((1 / c) to_power a) by A4, XREAL_1:68;
then (1 / c) to_power b > (1 / c) to_power a by A5, XCMPLX_1:87;
then (1 to_power b) / (c to_power b) > (1 / c) to_power a by A2, Th31;
then 1 / (c to_power b) > (1 / c) to_power a by Th26;
then 1 / (c to_power b) > (1 to_power a) / (c to_power a) by A2, Th31;
then 1 / (c to_power b) > 1 / (c to_power a) by Th26;
hence c to_power a > c to_power b by A6, XREAL_1:91; :: thesis: verum