Theorem reglogcl

Description: General logarithm is a real number. (Contributed by Stefan O'Rear, 19-Sep-2014) (New usage is discouraged.) Use relogbcl instead.

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

Proof

Step	Hyp	Ref	Expression
1		relogcl	|- ( A e. RR+ -> ( log ` A ) e. RR )
2	1	3ad2ant1	|- ( ( A e. RR+ /\ B e. RR+ /\ B =/= 1 ) -> ( log ` A ) e. RR )
3		relogcl	|- ( B e. RR+ -> ( log ` B ) e. RR )
4	3	3ad2ant2	|- ( ( A e. RR+ /\ B e. RR+ /\ B =/= 1 ) -> ( log ` B ) e. RR )
5		logne0	|- ( ( B e. RR+ /\ B =/= 1 ) -> ( log ` B ) =/= 0 )
6	5	3adant1	|- ( ( A e. RR+ /\ B e. RR+ /\ B =/= 1 ) -> ( log ` B ) =/= 0 )
7	2 4 6	redivcld	|- ( ( A e. RR+ /\ B e. RR+ /\ B =/= 1 ) -> ( ( log ` A ) / ( log ` B ) ) e. RR )