let a, b, c be real number ; :: thesis: ( a < b & c > 0 & c < 1 implies c to_power a > c to_power b )
assume A1: ( a < b & c > 0 & c < 1 ) ; :: thesis: c to_power a > c to_power b
then A2: 1 / c > 0 ;
then A3: (1 / c) to_power a > 0 by Th39;
A4: (1 / c) to_power a <> 0 by A2, Th39;
c to_power a > 0 by A1, Th39;
then A5: 1 / (c to_power a) > 0 ;
c / c < 1 / c by A1, XREAL_1:76;
then A6: 1 < 1 / c by A1, XCMPLX_1:60;
b - a > 0 by A1, XREAL_1:52;
then (1 / c) to_power (b - a) > 1 by A6, Th40;
then ((1 / c) to_power b) / ((1 / c) to_power a) > 1 by A1, Th34;
then (((1 / c) to_power b) / ((1 / c) to_power a)) * ((1 / c) to_power a) > 1 * ((1 / c) to_power a) by A3, XREAL_1:70;
then (1 / c) to_power b > (1 / c) to_power a by A4, XCMPLX_1:88;
then (1 to_power b) / (c to_power b) > (1 / c) to_power a by A1, Th36;
then 1 / (c to_power b) > (1 / c) to_power a by Th31;
then 1 / (c to_power b) > (1 to_power a) / (c to_power a) by A1, Th36;
then 1 / (c to_power b) > 1 / (c to_power a) by Th31;
hence c to_power a > c to_power b by A5, XREAL_1:93; :: thesis: verum