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