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 & z <> +infty ) ; :: thesis: x / z < y / z
A3: ( x <> +infty & y <> -infty ) by A1, XXREAL_0:4, XXREAL_0:5;
reconsider c = z as Real by A2, XXREAL_0:14;
now
per cases ( y <> +infty or y = +infty ) ;
suppose y <> +infty ; :: thesis: x / z < y / z
then reconsider b = y as Real by A3, XXREAL_0:14;
A4: y / z = b / c by A2, Th32;
now
per cases ( x <> -infty or x = -infty ) ;
suppose x <> -infty ; :: thesis: x / z < y / z
then reconsider a = x as Real by A3, XXREAL_0:14;
x / z = a / c by A2, Th32;
hence x / z < y / z by A1, A2, A4, XREAL_1:76; :: thesis: verum
end;
end;
end;
hence x / z < y / z ; :: thesis: verum
end;
suppose y = +infty ; :: thesis: x / z < y / z
then A5: y / z = +infty by A2, Def2;
now
per cases ( x <> -infty or x = -infty ) ;
suppose x <> -infty ; :: thesis: x / z < y / z
then reconsider a = x as Real by A3, XXREAL_0:14;
x / z = a / c by A2, Th32;
hence x / z < y / z by A5, XXREAL_0:9; :: thesis: verum
end;
suppose x = -infty ; :: thesis: x / z < y / z
hence x / z < y / z by A2, A5, Def2; :: thesis: verum
end;
end;
end;
hence x / z < y / z ; :: thesis: verum
end;
end;
end;
hence x / z < y / z ; :: thesis: verum