let a, b, n be non negative Real; :: thesis: ( max ((a to_power n),(b to_power n)) = (max (a,b)) to_power n & min ((a to_power n),(b to_power n)) = (min (a,b)) to_power n )

per cases ( n is zero or not n is zero ) ;

suppose n is zero ; :: thesis: ( max ((a to_power n),(b to_power n)) = (max (a,b)) to_power n & min ((a to_power n),(b to_power n)) = (min (a,b)) to_power n )

then ( (max (a,b)) to_power n = 1 & (min (a,b)) to_power n = 1 & a to_power n = 1 & b to_power n = 1 ) by POWER:24;
hence ( max ((a to_power n),(b to_power n)) = (max (a,b)) to_power n & min ((a to_power n),(b to_power n)) = (min (a,b)) to_power n ) ; :: thesis: verum

end;

suppose not n is zero ; :: thesis: ( max ((a to_power n),(b to_power n)) = (max (a,b)) to_power n & min ((a to_power n),(b to_power n)) = (min (a,b)) to_power n )

then reconsider n = n as positive Real ;

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

suppose B1: a >= b ; :: thesis: ( max ((a to_power n),(b to_power n)) = (max (a,b)) to_power n & min ((a to_power n),(b to_power n)) = (min (a,b)) to_power n )

then B2: ( max (a,b) = a & min (a,b) = b ) by XXREAL_0:def 9, XXREAL_0:def 10;
a to_power n >= b to_power n by B1, POWER37;
hence ( max ((a to_power n),(b to_power n)) = (max (a,b)) to_power n & min ((a to_power n),(b to_power n)) = (min (a,b)) to_power n ) by B2, XXREAL_0:def 9, XXREAL_0:def 10; :: thesis: verum

end;

suppose B1: a < b ; :: thesis: ( max ((a to_power n),(b to_power n)) = (max (a,b)) to_power n & min ((a to_power n),(b to_power n)) = (min (a,b)) to_power n )

then B2: ( max (a,b) = b & min (a,b) = a ) by XXREAL_0:def 9, XXREAL_0:def 10;
a to_power n < b to_power n by B1, POWER37;
hence ( max ((a to_power n),(b to_power n)) = (max (a,b)) to_power n & min ((a to_power n),(b to_power n)) = (min (a,b)) to_power n ) by B2, XXREAL_0:def 9, XXREAL_0:def 10; :: thesis: verum

end;

end;

end;

end;