let c be Nat; :: thesis: ( c > 0 implies for r, s being non negative Real holds
( r < s iff r |^ c < s |^ c ) )
assume A0: c > 0 ; :: thesis: for r, s being non negative Real holds
( r < s iff r |^ c < s |^ c )
let r, s be non negative Real; :: thesis: ( r < s iff r |^ c < s |^ c )
( ( r < s implies r |^ c < s |^ c ) & ( r |^ c < s |^ c implies r < s ) )
proof
A0a: ( r < s implies r |^ c < s |^ c )
proof
assume A1: r < s ; :: thesis: r |^ c < s |^ c
then s |^ c > 0 by PREPOWER:6;
then A2: ( r = 0 implies s |^ c > r |^ c ) by A0, NAT_1:14, NEWTON:11;
( r > 0 implies r to_power c < s to_power c ) by A0, A1, POWER:37;
hence r |^ c < s |^ c by A2; :: thesis: verum
end;
( s = 0 implies s |^ c = 0 ) by A0, NAT_1:14, NEWTON:11;
then ( r > 0 & s = 0 implies r |^ c > s |^ c ) by PREPOWER:6;
hence ( ( r < s implies r |^ c < s |^ c ) & ( r |^ c < s |^ c implies r < s ) ) by A0a, PREPOWER:9; :: thesis: verum
end;
hence ( r < s iff r |^ c < s |^ c ) ; :: thesis: verum