let a, b, c be Real; ( a > 0 & a <> 1 & b > 0 & c > 0 implies (log (a,b)) - (log (a,c)) = log (a,(b / c)) )
assume that
A1:
a > 0
and
A2:
a <> 1
and
A3:
b > 0
and
A4:
c > 0
; (log (a,b)) - (log (a,c)) = log (a,(b / c))
A5: a to_power ((log (a,b)) - (log (a,c))) =
(a to_power (log (a,b))) / (a to_power (log (a,c)))
by A1, Th29
.=
b / (a to_power (log (a,c)))
by A1, A2, A3, Def3
.=
b / c
by A1, A2, A4, Def3
;
b / c > 0
by A3, A4, XREAL_1:139;
hence
(log (a,b)) - (log (a,c)) = log (a,(b / c))
by A1, A2, A5, Def3; verum