let x, y, z be ExtReal; :: thesis: ( x is real & not y is real implies x * (y + z) = (x * y) + (x * z) )
assume that
A1: x is real and
A2: not y is real ; :: thesis: x * (y + z) = (x * y) + (x * z)
per cases ( z is real or not z is real ) ;
suppose z is real ; :: thesis: x * (y + z) = (x * y) + (x * z)
hence x * (y + z) = (x * y) + (x * z) by A1, Lm27; :: thesis: verum
end;
suppose not z is real ; :: thesis: x * (y + z) = (x * y) + (x * z)
then A3: not z in REAL ;
A4: not y in REAL by A2;
per cases ( ( y = -infty & z = -infty ) or ( y = -infty & z = +infty ) or ( y = +infty & z = -infty ) or ( y = +infty & z = +infty ) ) by A4, A3, XXREAL_0:14;
suppose ( y = -infty & z = -infty ) ; :: thesis: x * (y + z) = (x * y) + (x * z)
hence x * (y + z) = (x * y) + (x * z) by Lm24; :: thesis: verum
end;
suppose ( y = -infty & z = +infty ) ; :: thesis: x * (y + z) = (x * y) + (x * z)
hence x * (y + z) = (x * y) + (x * z) by Th5, Th93; :: thesis: verum
end;
suppose ( y = +infty & z = -infty ) ; :: thesis: x * (y + z) = (x * y) + (x * z)
hence x * (y + z) = (x * y) + (x * z) by Th6, Th93; :: thesis: verum
end;
suppose ( y = +infty & z = +infty ) ; :: thesis: x * (y + z) = (x * y) + (x * z)
hence x * (y + z) = (x * y) + (x * z) by Lm24; :: thesis: verum
end;
end;
end;
end;