let p be Real; :: thesis: ( 0 <= p implies for a, b being Real st 0 <= a & a <= b holds
a to_power p <= b to_power p )
assume A1: 0 <= p ; :: thesis: for a, b being Real st 0 <= a & a <= b holds
a to_power p <= b to_power p
let a, b be Real; :: thesis: ( 0 <= a & a <= b implies a to_power p <= b to_power p )
assume that
A2: 0 <= a and
A3: a <= b ; :: thesis: a to_power p <= b to_power p

per cases ( 0 = p or 0 < p ) by A1;

suppose S1: 0 = p ; :: thesis: a to_power p <= b to_power p

( a to_power 0 = 1 & b to_power 0 = 1 ) by POWER:24;
hence a to_power p <= b to_power p by S1; :: thesis: verum

end;

suppose S2: 0 < p ; :: thesis: a to_power p <= b to_power p

per cases ( a = b or a <> b ) ;

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

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

end;

suppose A4: a <> b ; :: thesis: a to_power p <= b to_power p

A5: a < b by A3, A4, XXREAL_0:1;

now :: thesis: a to_power p <= b to_power p

per cases ( a = 0 or a <> 0 ) ;

suppose A6: a = 0 ; :: thesis: a to_power p <= b to_power p

then a to_power p = 0 by S2, POWER:def 2;
hence a to_power p <= b to_power p by A3, A4, A6, POWER:34; :: thesis: verum

end;

suppose a <> 0 ; :: thesis: a to_power p <= b to_power p

hence a to_power p <= b to_power p by A2, A5, S2, POWER:37; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

end;