let x, y, z be R_eal; :: thesis: ( x <= y & 0. <= z implies x * z <= y * z )
assume that
A1: x <= y and
A2: 0. <= z ; :: thesis: x * z <= y * z
per cases ( z = 0. or 0. < z ) by A2;
suppose z = 0. ; :: thesis: x * z <= y * z
then ( x * z = 0. & y * z = 0. ) by Def1;
hence x * z <= y * z ; :: thesis: verum
end;
suppose A3: 0. < z ; :: thesis: x * z <= y * z
now
per cases ( ( x < +infty & -infty < y ) or not x < +infty or not -infty < y ) ;
suppose A4: ( x < +infty & -infty < y ) ; :: thesis: x * z <= y * z
now
per cases ( z = +infty or z <> +infty ) ;
suppose A5: z = +infty ; :: thesis: x * z <= y * z
now
per cases ( x = 0. or x < 0. or 0. < x ) ;
suppose A6: x = 0. ; :: thesis: x * z <= y * z
then A7: ( x * z = 0. & 0. <= y ) by A1, Def1;
now
per cases ( 0. = y or 0. < y ) by A1, A6;
suppose 0. = y ; :: thesis: x * z <= y * z
hence x * z <= y * z by A6; :: thesis: verum
end;
suppose 0. < y ; :: thesis: x * z <= y * z
hence x * z <= y * z by A3, A7, Th20; :: thesis: verum
end;
end;
end;
hence x * z <= y * z ; :: thesis: verum
end;
suppose x < 0. ; :: thesis: x * z <= y * z
then x * z = -infty by A5, Def1;
hence x * z <= y * z by XXREAL_0:5; :: thesis: verum
end;
suppose A8: 0. < x ; :: thesis: x * z <= y * z
then A9: x * z = +infty by A5, Def1;
now
per cases ( y = x or x < y ) by A1, XXREAL_0:1;
suppose y = x ; :: thesis: x * z <= y * z
hence x * z <= y * z ; :: thesis: verum
end;
suppose x < y ; :: thesis: x * z <= y * z
hence x * z <= y * z by A5, A8, A9, Def1; :: thesis: verum
end;
end;
end;
hence x * z <= y * z ; :: thesis: verum
end;
end;
end;
hence x * z <= y * z ; :: thesis: verum
end;
suppose z <> +infty ; :: thesis: x * z <= y * z
then reconsider c = z as Real by A3, XXREAL_0:14;
now
per cases ( x = -infty or x <> -infty ) ;
suppose x <> -infty ; :: thesis: x * z <= y * z
then A10: x is Real by A4, XXREAL_0:14;
now
per cases ( y = +infty or y <> +infty ) ;
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
A11: ( a = x & b = y & a <= b ) by A1, A10;
( x * z = a * c & y * z = b * c ) by A11, Th13;
hence x * z <= y * z by A3, A11, XREAL_1:66; :: thesis: verum
end;
end;
end;
hence x * z <= y * z ; :: thesis: verum
end;
end;
end;
hence x * z <= y * z ; :: thesis: verum
end;
end;
end;
hence x * z <= y * z ; :: thesis: verum
end;
end;
end;
hence x * z <= y * z ; :: thesis: verum
end;
end;