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 ) & ( not y = -infty or not z = +infty ) & ( not x = +infty or not z = +infty ) & ( not x = -infty or not z = -infty ) implies (x - y) - z = 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: ( not y = -infty or not z = +infty ) and
A5: ( not x = +infty or not z = +infty ) and
A6: ( not x = -infty or not z = -infty ) ; :: thesis: (x - y) - z = x - (y + z)
per cases ( x = +infty or x = -infty or ( x <> +infty & x <> -infty ) ) ;
suppose A7: x = +infty ; :: thesis: (x - y) - z = x - (y + z)
then x - y = +infty by A1, Th13;
then A8: (x - y) - z = +infty by A5, A7, Th13;
y + z <> +infty by A1, A5, A7, Lm8;
hence (x - y) - z = x - (y + z) by A7, A8, Th13; :: thesis: verum
end;
suppose A9: x = -infty ; :: thesis: (x - y) - z = x - (y + z)
then x - y = -infty by A2, Th14;
then A10: (x - y) - z = -infty by A6, A9, Th14;
y + z <> -infty by A2, A6, A9, Lm9;
hence (x - y) - z = x - (y + z) by A9, A10, Th14; :: thesis: verum
end;
suppose A11: ( x <> +infty & x <> -infty ) ; :: thesis: (x - y) - z = x - (y + z)
then x in REAL by XXREAL_0:14;
then reconsider a = x as Real ;
per cases ( y = +infty or y = -infty or ( y <> +infty & y <> -infty ) ) ;
suppose A12: y = +infty ; :: thesis: (x - y) - z = x - (y + z)
then ( x - y = -infty & y + z = +infty ) by A3, A11, Def2, Th13;
hence (x - y) - z = x - (y + z) by A3, A12, Th14; :: thesis: verum
end;
suppose A13: y = -infty ; :: thesis: (x - y) - z = x - (y + z)
then ( x - y = +infty & y + z = -infty ) by A4, A11, Def2, Th14;
hence (x - y) - z = x - (y + z) by A4, A13, Th13; :: thesis: verum
end;
suppose ( y <> +infty & y <> -infty ) ; :: thesis: (x - y) - z = x - (y + z)
then y in REAL by XXREAL_0:14;
then reconsider b = y as Real ;
A14: x - y = a - b ;
per cases ( z = +infty or z = -infty or ( z <> +infty & z <> -infty ) ) ;
suppose z = +infty ; :: thesis: (x - y) - z = x - (y + z)
then ( (x - y) - z = -infty & y + z = +infty ) by A14, Def2, Th13;
hence (x - y) - z = x - (y + z) by A11, Th13; :: thesis: verum
end;
suppose z = -infty ; :: thesis: (x - y) - z = x - (y + z)
then ( (x - y) - z = +infty & y + z = -infty ) by A14, Def2, Th14;
hence (x - y) - z = x - (y + z) by A11, Th14; :: thesis: verum
end;
suppose ( z <> +infty & z <> -infty ) ; :: thesis: (x - y) - z = x - (y + z)
then z in REAL by XXREAL_0:14;
then reconsider c = z as Real ;
( (x - y) - z = (a - b) - c & x - (y + z) = a - (b + c) ) ;
hence (x - y) - z = x - (y + z) ; :: thesis: verum
end;
end;
end;
end;
end;
end;