let x, y, z be ExtReal; :: thesis: ( ( not x = +infty or not y = -infty ) & ( not x = -infty or not y = +infty ) & ( not y = +infty or not z = +infty ) & x <= z - y implies ( y <> +infty & x + y <= z ) )
assume that
A1: ( not x = +infty or not y = -infty ) and
A2: ( not x = -infty or not y = +infty ) and
A3: ( not y = +infty or not z = +infty ) and
A4: x <= z - y ; :: thesis: ( y <> +infty & x + y <= z )
thus A5: y <> +infty :: thesis: x + y <= z
proof
assume A6: y = +infty ; :: thesis: contradiction
then z - y = -infty by A3, Th13;
hence contradiction by A2, A4, A6, XXREAL_0:6; :: thesis: verum
end;
per cases ( y = -infty or ( y <> +infty & y <> -infty ) ) by A5;
suppose y = -infty ; :: thesis: x + y <= z
then x + y = -infty by A1, Def2;
hence x + y <= z by XXREAL_0:5; :: thesis: verum
end;
suppose A7: ( y <> +infty & y <> -infty ) ; :: thesis: x + y <= z
- -infty = +infty by Def3;
then A8: - y <> -infty by A7;
- +infty = -infty by Def3;
then - y <> +infty by A7;
then (z - y) + y = z + ((- y) + y) by A7, A8, Th29
.= z + 0 by Th7
.= z by Th4 ;
hence x + y <= z by A4, Th36; :: thesis: verum
end;
end;