let a be positive non weightless Real; :: thesis: for b being positive Real holds
( log (a,b) = - (log ((1 / a),b)) & log ((1 / a),b) = log (a,(1 / b)) & log (a,b) = - (log (a,(1 / b))) & log (a,b) = log ((1 / a),(1 / b)) )
let b be positive Real; :: thesis: ( log (a,b) = - (log ((1 / a),b)) & log ((1 / a),b) = log (a,(1 / b)) & log (a,b) = - (log (a,(1 / b))) & log (a,b) = log ((1 / a),(1 / b)) )
A1: a <> 1 by TA1;
reconsider x = 1 / a as positive Real ;
A3: 1 / a <> 1 / 1 ;
A5: x to_power (- 1) = a to_power (- (- 1)) by POWER:32;
A6: log (x,b) = (log (x,a)) * (log (a,b)) by A3, POWER:56
.= ((- 1) * 1) * (log (a,b)) by A5 ;
A7: (1 / b) to_power 1 = b to_power (- 1) by POWER:32;
then A8: log (a,(1 / b)) = (- 1) * (log (a,b)) by A1, POWER:55;
log (x,(1 / b)) = (- 1) * (log (x,b)) by A3, A7, POWER:55;
hence ( log (a,b) = - (log ((1 / a),b)) & log ((1 / a),b) = log (a,(1 / b)) & log (a,b) = - (log (a,(1 / b))) & log (a,b) = log ((1 / a),(1 / b)) ) by A6, A8; :: thesis: verum