let a, b, c be Real; :: thesis: ( a > 0 & a <> 1 & b >= 0 & c >= 0 implies (b * c) * (log (a,(b * c))) = ((b * c) * (log (a,b))) + ((b * c) * (log (a,c))) )
assume that
A1: a > 0 and
A2: a <> 1 and
A3: b >= 0 and
A4: c >= 0 ; :: thesis: (b * c) * (log (a,(b * c))) = ((b * c) * (log (a,b))) + ((b * c) * (log (a,c)))
per cases ( ( b > 0 & c = 0 ) or ( b = 0 & c = 0 ) or ( b = 0 & c > 0 ) or ( b > 0 & c > 0 ) ) by A3, A4;
suppose ( b > 0 & c = 0 ) ; :: thesis: (b * c) * (log (a,(b * c))) = ((b * c) * (log (a,b))) + ((b * c) * (log (a,c)))
hence (b * c) * (log (a,(b * c))) = ((b * c) * (log (a,b))) + ((b * c) * (log (a,c))) ; :: thesis: verum
end;
suppose ( b = 0 & c = 0 ) ; :: thesis: (b * c) * (log (a,(b * c))) = ((b * c) * (log (a,b))) + ((b * c) * (log (a,c)))
hence (b * c) * (log (a,(b * c))) = ((b * c) * (log (a,b))) + ((b * c) * (log (a,c))) ; :: thesis: verum
end;
suppose ( b = 0 & c > 0 ) ; :: thesis: (b * c) * (log (a,(b * c))) = ((b * c) * (log (a,b))) + ((b * c) * (log (a,c)))
hence (b * c) * (log (a,(b * c))) = ((b * c) * (log (a,b))) + ((b * c) * (log (a,c))) ; :: thesis: verum
end;
suppose ( b > 0 & c > 0 ) ; :: thesis: (b * c) * (log (a,(b * c))) = ((b * c) * (log (a,b))) + ((b * c) * (log (a,c)))
hence (b * c) * (log (a,(b * c))) = (b * c) * ((log (a,b)) + (log (a,c))) by A1, A2, POWER:53
.= ((b * c) * (log (a,b))) + ((b * c) * (log (a,c))) ;
:: thesis: verum
end;
end;