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 ) )

( 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

hence
( r < s iff r |^ c < s |^ c )
; :: thesis: verum
A0a:
( r < s implies r |^ c < s |^ c )

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;proof

( s = 0 implies s |^ c = 0 )
by A0, NAT_1:14, NEWTON:11;
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;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

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