let a, b, c be Real; :: thesis: ( 0 < a & a <= b & c >= 0 implies a to_power c <= b to_power c )
assume that
A1: 0 < a and
A2: a <= b and
A3: c >= 0 ; :: thesis: a to_power c <= b to_power c

per cases ( c = 0 or c > 0 ) by A3;

suppose A4: c = 0 ; :: thesis: a to_power c <= b to_power c

then a to_power c = 1 by POWER:24;
hence a to_power c <= b to_power c by A4, POWER:24; :: thesis: verum

end;

suppose A5: c > 0 ; :: thesis: a to_power c <= b to_power c

per cases ( a = b or a < b ) by A2, XXREAL_0:1;

suppose a = b ; :: thesis: a to_power c <= b to_power c

hence a to_power c <= b to_power c ; :: thesis: verum

end;

suppose a < b ; :: thesis: a to_power c <= b to_power c

hence a to_power c <= b to_power c by A1, A5, POWER:37; :: thesis: verum

end;

end;

end;

end;