let a, b, c be real number ; ( 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
; c to_power a > c to_power b
A4:
(1 / c) to_power a > 0
by A2, Th39;
A5:
(1 / c) to_power a <> 0
by A2, Th39;
A6:
c to_power a > 0
by A2, Th39;
A7:
c / c < 1 / c
by A2, A3, XREAL_1:76;
A8:
1 < 1 / c
by A2, A7, XCMPLX_1:60;
A9:
b - a > 0
by A1, XREAL_1:52;
A10:
(1 / c) to_power (b - a) > 1
by A8, A9, Th40;
A11:
((1 / c) to_power b) / ((1 / c) to_power a) > 1
by A2, A10, Th34;
A12:
(((1 / c) to_power b) / ((1 / c) to_power a)) * ((1 / c) to_power a) > 1 * ((1 / c) to_power a)
by A4, A11, XREAL_1:70;
A13:
(1 / c) to_power b > (1 / c) to_power a
by A5, A12, XCMPLX_1:88;
A14:
(1 to_power b) / (c to_power b) > (1 / c) to_power a
by A2, A13, Th36;
A15:
1 / (c to_power b) > (1 / c) to_power a
by A14, Th31;
A16:
1 / (c to_power b) > (1 to_power a) / (c to_power a)
by A2, A15, Th36;
A17:
1 / (c to_power b) > 1 / (c to_power a)
by A16, Th31;
thus
c to_power a > c to_power b
by A6, A17, XREAL_1:93; verum