let x, y, z be ExtReal; :: thesis: ( ( z = +infty & y = +infty ) or ( z = -infty & y = -infty ) or not x < z - y or ( x <> +infty & y <> +infty & z <> -infty & x + y < z ) )
assume that
A1: ( not ( z = +infty & y = +infty ) & not ( z = -infty & y = -infty ) ) and
A2: x < z - y ; :: thesis: ( x <> +infty & y <> +infty & z <> -infty & x + y < z )
per cases ( x = -infty or x <> -infty ) ;
suppose A3: x = -infty ; :: thesis: ( x <> +infty & y <> +infty & z <> -infty & x + y < z )
A4: -infty <= z by XXREAL_0:5;
z <> -infty by A1, A2, A3, Th14;
then A5: -infty < z by A4, XXREAL_0:1;
y <> +infty by A1, A2, A3, Th13;
hence ( x <> +infty & y <> +infty & z <> -infty & x + y < z ) by A3, A5, Def2; :: thesis: verum
end;
suppose A6: x <> -infty ; :: thesis: ( x <> +infty & y <> +infty & z <> -infty & x + y < z )
A7: z - y <= +infty by XXREAL_0:4;
then x in REAL by A2, A6, XXREAL_0:14;
then reconsider a = x as Real ;
A8: -infty <= x by XXREAL_0:5;
then A9: z <> -infty by A1, A2, Th14;
A10: y <> +infty by A1, A2, A8, Th13;
per cases ( y = -infty or y <> -infty ) ;
suppose y <> -infty ; :: thesis: ( x <> +infty & y <> +infty & z <> -infty & x + y < z )
then y in REAL by A10, XXREAL_0:14;
then reconsider b = y as Real ;
per cases ( z = +infty or z <> +infty ) ;
suppose z <> +infty ; :: thesis: ( x <> +infty & y <> +infty & z <> -infty & x + y < z )
then z in REAL by A9, XXREAL_0:14;
then reconsider c = z as Real ;
z - y = c - b ;
then a + b < c by A2, XREAL_1:20;
hence ( x <> +infty & y <> +infty & z <> -infty & x + y < z ) ; :: thesis: verum
end;
end;
end;
end;
end;
end;