let a, b be Real; :: thesis: ( a > 0 & a <> 1 & b > 0 implies - (log (a,b)) = log (a,(1 / b)) )
assume that
A1: a > 0 and
A2: a <> 1 and
A3: b > 0 ; :: thesis: - (log (a,b)) = log (a,(1 / b))
thus - (log (a,b)) = 0 - (log (a,b))
.= (log (a,1)) - (log (a,b)) by A1, A2, POWER:51
.= log (a,(1 / b)) by A1, A2, A3, POWER:54 ; :: thesis: verum