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

Metamath Proof Explorer

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 )