Theorem relogbcld

Description: Closure of the general logarithm with a positive real base on positive reals, a deduction version. (Contributed by metakunt, 22-May-2024)

	Ref	Expression
Hypotheses	relogbcld.1	|- ( ph -> B e. RR )
	relogbcld.2	|- ( ph -> 0 < B )
	relogbcld.3	|- ( ph -> X e. RR )
	relogbcld.4	|- ( ph -> 0 < X )
	relogbcld.5	|- ( ph -> B =/= 1 )
Assertion	relogbcld	|- ( ph -> ( B logb X ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		relogbcld.1	|- ( ph -> B e. RR )
2		relogbcld.2	|- ( ph -> 0 < B )
3		relogbcld.3	|- ( ph -> X e. RR )
4		relogbcld.4	|- ( ph -> 0 < X )
5		relogbcld.5	|- ( ph -> B =/= 1 )
6	1 2	elrpd	|- ( ph -> B e. RR+ )
7	3 4	elrpd	|- ( ph -> X e. RR+ )
8	6 7 5	3jca	|- ( ph -> ( B e. RR+ /\ X e. RR+ /\ B =/= 1 ) )
9		relogbcl	|- ( ( B e. RR+ /\ X e. RR+ /\ B =/= 1 ) -> ( B logb X ) e. RR )
10	8 9	syl	|- ( ph -> ( B logb X ) e. RR )