let x, y, z be R_eal; :: thesis: ( x < y & 0. < z & z <> +infty implies x * z < y * z )
assume that
A1: x < y and
A2: 0. < z and
A3: z <> +infty ; :: thesis: x * z < y * z
A4: ( x < +infty & -infty < y )

proof

assume A5: ( not x < +infty or not -infty < y ) ; :: thesis: contradiction

now

per cases ( x = +infty or y = -infty ) by A5, XXREAL_0:4, XXREAL_0:6;

suppose x = +infty ; :: thesis: contradiction

hence contradiction by A1, XXREAL_0:4; :: thesis: verum

end;

suppose y = -infty ; :: thesis: contradiction

hence contradiction by A1, XXREAL_0:5; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

reconsider c = z as Real by A2, A3, XXREAL_0:14;

now

per cases ( x = -infty or x <> -infty ) ;

suppose x = -infty ; :: thesis: x * z < y * z

then A6: x * z = -infty by A2, Def1;

now

per cases ( y = +infty or y <> +infty ) ;

suppose y = +infty ; :: thesis: x * z < y * z

hence x * z < y * z by A2, A6, Def1; :: thesis: verum

end;

suppose y <> +infty ; :: thesis: x * z < y * z

then reconsider b = y as Real by A4, XXREAL_0:14;
y * z = b * c by Th13;
hence x * z < y * z by A6, XXREAL_0:12; :: thesis: verum

end;

end;

end;

hence x * z < y * z ; :: thesis: verum

end;

suppose A7: x <> -infty ; :: thesis: x * z < y * z

then A8: x is Real by A4, XXREAL_0:14;
reconsider a = x as Real by A4, A7, XXREAL_0:14;
A9: x * z = a * c by Th13;

now

per cases ( y = +infty or y <> +infty ) ;

suppose y = +infty ; :: thesis: x * z < y * z

then y * z = +infty by A2, Def1;
hence x * z < y * z by A9, XXREAL_0:9; :: thesis: verum

end;

suppose y <> +infty ; :: thesis: x * z < y * z

then y is Real by A4, XXREAL_0:14;
then consider a, b being Real such that
A10: ( a = x & b = y & a <= b ) by A1, A8;
( x * z = a * c & y * z = b * c ) by A10, Th13;
hence x * z < y * z by A1, A2, A10, XREAL_1:70; :: thesis: verum

end;

end;

end;

hence x * z < y * z ; :: thesis: verum

end;

end;

end;

hence x * z < y * z ; :: thesis: verum