This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )