let x, y, k be ExtReal; :: thesis: ( 0 <= k implies ( k * (max (x,y)) = max ((k * x),(k * y)) & k * (min (x,y)) = min ((k * x),(k * y)) ) )
assume A1: 0 <= k ; :: thesis: ( k * (max (x,y)) = max ((k * x),(k * y)) & k * (min (x,y)) = min ((k * x),(k * y)) )
now :: thesis: k * (max (x,y)) = max ((k * x),(k * y))
per cases ( max (x,y) = x or max (x,y) = y ) by XXREAL_0:16;
suppose A2: max (x,y) = x ; :: thesis: k * (max (x,y)) = max ((k * x),(k * y))
then y <= x by XXREAL_0:def 10;
then k * y <= k * x by A1, XXREAL_3:71;
hence k * (max (x,y)) = max ((k * x),(k * y)) by A2, XXREAL_0:def 10; :: thesis: verum
end;
suppose A3: max (x,y) = y ; :: thesis: k * (max (x,y)) = max ((k * x),(k * y))
then x <= y by XXREAL_0:def 10;
then k * x <= k * y by A1, XXREAL_3:71;
hence k * (max (x,y)) = max ((k * x),(k * y)) by A3, XXREAL_0:def 10; :: thesis: verum
end;
end;
end;
hence k * (max (x,y)) = max ((k * x),(k * y)) ; :: thesis: k * (min (x,y)) = min ((k * x),(k * y))
per cases ( min (x,y) = x or min (x,y) = y ) by XXREAL_0:15;
suppose A4: min (x,y) = x ; :: thesis: k * (min (x,y)) = min ((k * x),(k * y))
then x <= y by XXREAL_0:def 9;
then k * x <= k * y by A1, XXREAL_3:71;
hence k * (min (x,y)) = min ((k * x),(k * y)) by A4, XXREAL_0:def 9; :: thesis: verum
end;
suppose A5: min (x,y) = y ; :: thesis: k * (min (x,y)) = min ((k * x),(k * y))
then y <= x by XXREAL_0:def 9;
then k * y <= k * x by A1, XXREAL_3:71;
hence k * (min (x,y)) = min ((k * x),(k * y)) by A5, XXREAL_0:def 9; :: thesis: verum
end;
end;