Theorem reglogmul

Description: Multiplication law for general log. (Contributed by Stefan O'Rear, 19-Sep-2014) (New usage is discouraged.) Use relogbmul instead.

	Ref	Expression
Assertion	reglogmul	|- ( ( A e. RR+ /\ B e. RR+ /\ ( C e. RR+ /\ C =/= 1 ) ) -> ( ( log ` ( A x. B ) ) / ( log ` C ) ) = ( ( ( log ` A ) / ( log ` C ) ) + ( ( log ` B ) / ( log ` C ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		relogmul	|- ( ( A e. RR+ /\ B e. RR+ ) -> ( log ` ( A x. B ) ) = ( ( log ` A ) + ( log ` B ) ) )
2	1	3adant3	|- ( ( A e. RR+ /\ B e. RR+ /\ ( C e. RR+ /\ C =/= 1 ) ) -> ( log ` ( A x. B ) ) = ( ( log ` A ) + ( log ` B ) ) )
3	2	oveq1d	|- ( ( A e. RR+ /\ B e. RR+ /\ ( C e. RR+ /\ C =/= 1 ) ) -> ( ( log ` ( A x. B ) ) / ( log ` C ) ) = ( ( ( log ` A ) + ( log ` B ) ) / ( log ` C ) ) )
4		relogcl	|- ( A e. RR+ -> ( log ` A ) e. RR )
5	4	recnd	|- ( A e. RR+ -> ( log ` A ) e. CC )
6	5	3ad2ant1	|- ( ( A e. RR+ /\ B e. RR+ /\ ( C e. RR+ /\ C =/= 1 ) ) -> ( log ` A ) e. CC )
7		relogcl	|- ( B e. RR+ -> ( log ` B ) e. RR )
8	7	recnd	|- ( B e. RR+ -> ( log ` B ) e. CC )
9	8	3ad2ant2	|- ( ( A e. RR+ /\ B e. RR+ /\ ( C e. RR+ /\ C =/= 1 ) ) -> ( log ` B ) e. CC )
10		relogcl	|- ( C e. RR+ -> ( log ` C ) e. RR )
11	10	recnd	|- ( C e. RR+ -> ( log ` C ) e. CC )
12	11	adantr	|- ( ( C e. RR+ /\ C =/= 1 ) -> ( log ` C ) e. CC )
13	12	3ad2ant3	|- ( ( A e. RR+ /\ B e. RR+ /\ ( C e. RR+ /\ C =/= 1 ) ) -> ( log ` C ) e. CC )
14		logne0	|- ( ( C e. RR+ /\ C =/= 1 ) -> ( log ` C ) =/= 0 )
15	14	3ad2ant3	|- ( ( A e. RR+ /\ B e. RR+ /\ ( C e. RR+ /\ C =/= 1 ) ) -> ( log ` C ) =/= 0 )
16	6 9 13 15	divdird	|- ( ( A e. RR+ /\ B e. RR+ /\ ( C e. RR+ /\ C =/= 1 ) ) -> ( ( ( log ` A ) + ( log ` B ) ) / ( log ` C ) ) = ( ( ( log ` A ) / ( log ` C ) ) + ( ( log ` B ) / ( log ` C ) ) ) )
17	3 16	eqtrd	|- ( ( A e. RR+ /\ B e. RR+ /\ ( C e. RR+ /\ C =/= 1 ) ) -> ( ( log ` ( A x. B ) ) / ( log ` C ) ) = ( ( ( log ` A ) / ( log ` C ) ) + ( ( log ` B ) / ( log ` C ) ) ) )