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;
A6:
a / a < b / a
by A1, A2, XREAL_1:76;
A7:
1 < b / a
by A1, A6, XCMPLX_1:60;
A8:
(b / a) to_power c > 1
by A3, A7, Th40;
A9:
(b to_power c) / (a to_power c) > 1
by A1, A2, A8, Th36;
A10:
((b to_power c) / (a to_power c)) * (a to_power c) > 1 * (a to_power c)
by A4, A9, XREAL_1:70;
thus
a to_power c < b to_power c
by A5, A10, XCMPLX_1:88; verum