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