let a, b, c be real number ; :: thesis: ( a > 0 & a <> 1 & b > 0 & b <> 1 & c > 0 implies log a,c = (log a,b) * (log b,c) )
assume that
A1: a > 0 and
A2: a <> 1 and
A3: b > 0 and
A4: b <> 1 and
A5: c > 0 ; :: thesis: log a,c = (log a,b) * (log b,c)
a to_power ((log a,b) * (log b,c)) = (a to_power (log a,b)) to_power (log b,c) by A1, Th38
.= b to_power (log b,c) by A1, A2, A3, Def3
.= c by A3, A4, A5, Def3 ;
hence log a,c = (log a,b) * (log b,c) by A1, A2, A5, Def3; :: thesis: verum