Theorem relogbzcl

Description: Closure of the general logarithm with integer base on positive reals. (Contributed by Thierry Arnoux, 27-Sep-2017) (Proof shortened by AV, 9-Jun-2020)

	Ref	Expression
Assertion	relogbzcl	|- ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ ) -> ( B logb X ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		zgt1rpn0n1	|- ( B e. ( ZZ>= ` 2 ) -> ( B e. RR+ /\ B =/= 0 /\ B =/= 1 ) )
2		relogbcl	|- ( ( B e. RR+ /\ X e. RR+ /\ B =/= 1 ) -> ( B logb X ) e. RR )
3	2	3com23	|- ( ( B e. RR+ /\ B =/= 1 /\ X e. RR+ ) -> ( B logb X ) e. RR )
4	3	3expia	|- ( ( B e. RR+ /\ B =/= 1 ) -> ( X e. RR+ -> ( B logb X ) e. RR ) )
5	4	3adant2	|- ( ( B e. RR+ /\ B =/= 0 /\ B =/= 1 ) -> ( X e. RR+ -> ( B logb X ) e. RR ) )
6	1 5	syl	|- ( B e. ( ZZ>= ` 2 ) -> ( X e. RR+ -> ( B logb X ) e. RR ) )
7	6	imp	|- ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ ) -> ( B logb X ) e. RR )