Theorem relogbcl

Description: Closure of the general logarithm with a positive real base on positive reals. (Contributed by Stefan O'Rear, 19-Sep-2014) (Revised by Thierry Arnoux, 27-Sep-2017)

	Ref	Expression
Assertion	relogbcl	|- ( ( B e. RR+ /\ X e. RR+ /\ B =/= 1 ) -> ( B logb X ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		simp1	|- ( ( B e. RR+ /\ X e. RR+ /\ B =/= 1 ) -> B e. RR+ )
2	1	rpcnne0d	|- ( ( B e. RR+ /\ X e. RR+ /\ B =/= 1 ) -> ( B e. CC /\ B =/= 0 ) )
3		simp3	|- ( ( B e. RR+ /\ X e. RR+ /\ B =/= 1 ) -> B =/= 1 )
4		df-3an	|- ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) <-> ( ( B e. CC /\ B =/= 0 ) /\ B =/= 1 ) )
5	2 3 4	sylanbrc	|- ( ( B e. RR+ /\ X e. RR+ /\ B =/= 1 ) -> ( B e. CC /\ B =/= 0 /\ B =/= 1 ) )
6		eldifpr	|- ( B e. ( CC \ { 0 , 1 } ) <-> ( B e. CC /\ B =/= 0 /\ B =/= 1 ) )
7	5 6	sylibr	|- ( ( B e. RR+ /\ X e. RR+ /\ B =/= 1 ) -> B e. ( CC \ { 0 , 1 } ) )
8		simp2	|- ( ( B e. RR+ /\ X e. RR+ /\ B =/= 1 ) -> X e. RR+ )
9	8	rpcnne0d	|- ( ( B e. RR+ /\ X e. RR+ /\ B =/= 1 ) -> ( X e. CC /\ X =/= 0 ) )
10		eldifsn	|- ( X e. ( CC \ { 0 } ) <-> ( X e. CC /\ X =/= 0 ) )
11	9 10	sylibr	|- ( ( B e. RR+ /\ X e. RR+ /\ B =/= 1 ) -> X e. ( CC \ { 0 } ) )
12		logbval	|- ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( B logb X ) = ( ( log ` X ) / ( log ` B ) ) )
13	7 11 12	syl2anc	|- ( ( B e. RR+ /\ X e. RR+ /\ B =/= 1 ) -> ( B logb X ) = ( ( log ` X ) / ( log ` B ) ) )
14		relogcl	|- ( X e. RR+ -> ( log ` X ) e. RR )
15	14	3ad2ant2	|- ( ( B e. RR+ /\ X e. RR+ /\ B =/= 1 ) -> ( log ` X ) e. RR )
16		relogcl	|- ( B e. RR+ -> ( log ` B ) e. RR )
17	16	3ad2ant1	|- ( ( B e. RR+ /\ X e. RR+ /\ B =/= 1 ) -> ( log ` B ) e. RR )
18		logne0	|- ( ( B e. RR+ /\ B =/= 1 ) -> ( log ` B ) =/= 0 )
19	18	3adant2	|- ( ( B e. RR+ /\ X e. RR+ /\ B =/= 1 ) -> ( log ` B ) =/= 0 )
20	15 17 19	redivcld	|- ( ( B e. RR+ /\ X e. RR+ /\ B =/= 1 ) -> ( ( log ` X ) / ( log ` B ) ) e. RR )
21	13 20	eqeltrd	|- ( ( B e. RR+ /\ X e. RR+ /\ B =/= 1 ) -> ( B logb X ) e. RR )