let x, y, z be ExtReal; :: thesis: ( x is real & y is real implies x * (y + z) = (x * y) + (x * z) )
assume that
A1: x is real and
A2: y is real ; :: thesis: x * (y + z) = (x * y) + (x * z)
reconsider r = x, s = y as Real by A1, A2;
A3: x * y = r * s ;
per cases ( z in REAL or z = -infty or z = +infty ) by XXREAL_0:14;
suppose z in REAL ; :: thesis: x * (y + z) = (x * y) + (x * z)
then reconsider t = z as Real ;
reconsider u = s + t, v = r * s, w = r * t as Real ;
r * u = v + w ;
hence x * (y + z) = (x * y) + (x * z) ; :: thesis: verum
end;
suppose A4: z = -infty ; :: thesis: x * (y + z) = (x * y) + (x * z)
then A5: y + z = -infty by A2, Def2;
per cases ( x is zero or x is positive or x is negative ) ;
suppose x is zero ; :: thesis: x * (y + z) = (x * y) + (x * z)
then x = 0 ;
hence x * (y + z) = (x * y) + (x * z) by Lm26; :: thesis: verum
end;
suppose A6: x is positive ; :: thesis: x * (y + z) = (x * y) + (x * z)
hence x * (y + z) = -infty by A5, Def5
.= (x * y) + -infty by A3, Def2
.= (x * y) + (x * z) by A4, A6, Def5 ;
:: thesis: verum
end;
suppose A7: x is negative ; :: thesis: x * (y + z) = (x * y) + (x * z)
hence x * (y + z) = +infty by A5, Def5
.= (x * y) + +infty by A3, Def2
.= (x * y) + (x * z) by A4, A7, Def5 ;
:: thesis: verum
end;
end;
end;
suppose A8: z = +infty ; :: thesis: x * (y + z) = (x * y) + (x * z)
then A9: y + z = +infty by A2, Def2;
per cases ( x is zero or x is positive or x is negative ) ;
suppose x is zero ; :: thesis: x * (y + z) = (x * y) + (x * z)
then x = 0 ;
hence x * (y + z) = (x * y) + (x * z) by Lm26; :: thesis: verum
end;
suppose A10: x is positive ; :: thesis: x * (y + z) = (x * y) + (x * z)
hence x * (y + z) = +infty by A9, Def5
.= (x * y) + +infty by A3, Def2
.= (x * y) + (x * z) by A8, A10, Def5 ;
:: thesis: verum
end;
suppose A11: x is negative ; :: thesis: x * (y + z) = (x * y) + (x * z)
hence x * (y + z) = -infty by A9, Def5
.= (x * y) + -infty by A3, Def2
.= (x * y) + (x * z) by A8, A11, Def5 ;
:: thesis: verum
end;
end;
end;
end;