let a, b, c be real number ; :: thesis: ( a > 0 & a <> 1 & b > 0 & c > 0 implies (log a,b) - (log a,c) = log a,(b / c) )
assume A1: ( a > 0 & a <> 1 & b > 0 & c > 0 ) ; :: thesis: (log a,b) - (log a,c) = log a,(b / c)
then A2: a to_power ((log a,b) - (log a,c)) = (a to_power (log a,b)) / (a to_power (log a,c)) by Th34
.= b / (a to_power (log a,c)) by A1, Def3
.= b / c by A1, Def3 ;
b / c > 0 by A1, XREAL_1:141;
hence (log a,b) - (log a,c) = log a,(b / c) by A1, A2, Def3; :: thesis: verum