let a, b, c be real number ; ( 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, Th39;
A5:
a to_power c <> 0
by A1, Th39;
a / a < b / a
by A1, A2, XREAL_1:76;
then
1 < b / a
by A1, XCMPLX_1:60;
then
(b / a) to_power c > 1
by A3, Th40;
then
(b to_power c) / (a to_power c) > 1
by A1, A2, Th36;
then
((b to_power c) / (a to_power c)) * (a to_power c) > 1 * (a to_power c)
by A4, XREAL_1:70;
hence
a to_power c < b to_power c
by A5, XCMPLX_1:88; verum