Metamath Proof Explorer

Theorem relogdiv

Description: The natural logarithm of the quotient of two positive real numbers is the difference of natural logarithms. Exercise 72(a) and Property 3 of Cohen p. 301, restricted to natural logarithms. (Contributed by Steve Rodriguez, 25-Nov-2007)

		Ref	Expression
	Assertion	relogdiv	\|- ( ( A e. RR+ /\ B e. RR+ ) -> ( log ` ( A / B ) ) = ( ( log ` A ) - ( log ` B ) ) )

Proof

Step	Hyp	Ref	Expression
1		efsub	\|- ( ( ( log ` A ) e. CC /\ ( log ` B ) e. CC ) -> ( exp ` ( ( log ` A ) - ( log ` B ) ) ) = ( ( exp ` ( log ` A ) ) / ( exp ` ( log ` B ) ) ) )
2		resubcl	\|- ( ( ( log ` A ) e. RR /\ ( log ` B ) e. RR ) -> ( ( log ` A ) - ( log ` B ) ) e. RR )
3	1 2	relogoprlem	\|- ( ( A e. RR+ /\ B e. RR+ ) -> ( log ` ( A / B ) ) = ( ( log ` A ) - ( log ` B ) ) )

Step

Hyp

Ref

Expression

efsub

 |-  ( ( ( log ` A ) e. CC /\ ( log ` B ) e. CC ) -> ( exp ` ( ( log ` A ) - ( log ` B ) ) ) = ( ( exp ` ( log ` A ) ) / ( exp ` ( log ` B ) ) ) )

resubcl

 |-  ( ( ( log ` A ) e. RR /\ ( log ` B ) e. RR ) -> ( ( log ` A ) - ( log ` B ) ) e. RR )

1 2

relogoprlem

 |-  ( ( A e. RR+ /\ B e. RR+ ) -> ( log ` ( A / B ) ) = ( ( log ` A ) - ( log ` B ) ) )