let x, y, z be ext-real number ; :: thesis: ( x <= y implies x + z <= y + z )
assume Z: x <= y ; :: thesis: x + z <= y + z
per cases ( ( x in REAL & y in REAL ) or ( x in REAL & y = +infty ) or ( x = -infty & y in REAL ) or ( x = -infty & y = +infty ) or x = +infty or y = -infty ) by XXREAL_0:14;
suppose T: ( x in REAL & y in REAL ) ; :: thesis: x + z <= y + z
per cases ( z = -infty or z in REAL or z = +infty ) by XXREAL_0:14;
suppose S: z = -infty ; :: thesis: x + z <= y + z
-infty <= y + z by XXREAL_0:5;
hence x + z <= y + z by S, T, Def3; :: thesis: verum
end;
suppose z in REAL ; :: thesis: x + z <= y + z
then reconsider x = x, y = y, z = z as real number by T;
x + z <= y + z by Z, XREAL_1:8;
hence x + z <= y + z ; :: thesis: verum
end;
suppose S: z = +infty ; :: thesis: x + z <= y + z
x + z <= +infty by XXREAL_0:3;
hence x + z <= y + z by S, T, Def3; :: thesis: verum
end;
end;
end;
suppose T: ( x in REAL & y = +infty ) ; :: thesis: x + z <= y + z
per cases ( z = -infty or z in REAL or z = +infty ) by XXREAL_0:14;
suppose S: z = -infty ; :: thesis: x + z <= y + z
-infty <= y + z by XXREAL_0:5;
hence x + z <= y + z by S, T, Def3; :: thesis: verum
end;
suppose S: z in REAL ; :: thesis: x + z <= y + z
x + z <= +infty by XXREAL_0:3;
hence x + z <= y + z by S, T, Def3; :: thesis: verum
end;
suppose z = +infty ; :: thesis: x + z <= y + z
hence x + z <= y + z by T, Lm5C, XXREAL_0:3; :: thesis: verum
end;
end;
end;
suppose T: ( x = -infty & y in REAL ) ; :: thesis: x + z <= y + z
per cases ( z = -infty or z in REAL or z = +infty ) by XXREAL_0:14;
suppose z = -infty ; :: thesis: x + z <= y + z
hence x + z <= y + z by T, Lm5D, XXREAL_0:5; :: thesis: verum
end;
suppose S: z in REAL ; :: thesis: x + z <= y + z
-infty <= y + z by XXREAL_0:5;
hence x + z <= y + z by S, T, Def3; :: thesis: verum
end;
suppose S: z = +infty ; :: thesis: x + z <= y + z
x + z <= +infty by XXREAL_0:3;
hence x + z <= y + z by S, T, Def3; :: thesis: verum
end;
end;
end;
suppose T: ( x = -infty & y = +infty ) ; :: thesis: x + z <= y + z
per cases ( z = -infty or z in REAL or z = +infty ) by XXREAL_0:14;
suppose z = -infty ; :: thesis: x + z <= y + z
hence x + z <= y + z by T, Lm5D; :: thesis: verum
end;
suppose S: z in REAL ; :: thesis: x + z <= y + z
-infty <= y + z by XXREAL_0:5;
hence x + z <= y + z by S, T, Def3; :: thesis: verum
end;
suppose z = +infty ; :: thesis: x + z <= y + z
hence x + z <= y + z by T, Lm5C; :: thesis: verum
end;
end;
end;
suppose x = +infty ; :: thesis: x + z <= y + z
hence x + z <= y + z by Z, XXREAL_0:4; :: thesis: verum
end;
suppose y = -infty ; :: thesis: x + z <= y + z
hence x + z <= y + z by Z, XXREAL_0:6; :: thesis: verum
end;
end;