Metamath Proof Explorer

Theorem logbgt0b

Description: The logarithm of a positive real number to a real base greater than 1 is positive iff the number is greater than 1. (Contributed by AV, 29-Dec-2022)

Ref Expression
Assertion logbgt0b 
|- ( ( A e. RR+ /\ ( B e. RR+ /\ 1 < B ) ) -> ( 0 < ( B logb A ) <-> 1 < A ) )

Proof

Step Hyp Ref Expression
1 rpcn 
 |-  ( B e. RR+ -> B e. CC )
2 1 adantr 
 |-  ( ( B e. RR+ /\ 1 < B ) -> B e. CC )
3 rpne0 
 |-  ( B e. RR+ -> B =/= 0 )
4 3 adantr 
 |-  ( ( B e. RR+ /\ 1 < B ) -> B =/= 0 )
5 1red 
 |-  ( B e. RR+ -> 1 e. RR )
6 ltne 
 |-  ( ( 1 e. RR /\ 1 < B ) -> B =/= 1 )
7 5 6 sylan 
 |-  ( ( B e. RR+ /\ 1 < B ) -> B =/= 1 )
8 eldifpr 
 |-  ( B e. ( CC \ { 0 , 1 } ) <-> ( B e. CC /\ B =/= 0 /\ B =/= 1 ) )
9 2 4 7 8 syl3anbrc 
 |-  ( ( B e. RR+ /\ 1 < B ) -> B e. ( CC \ { 0 , 1 } ) )
10 rpcndif0 
 |-  ( A e. RR+ -> A e. ( CC \ { 0 } ) )
11 logbval 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ A e. ( CC \ { 0 } ) ) -> ( B logb A ) = ( ( log ` A ) / ( log ` B ) ) )
12 9 10 11 syl2anr 
 |-  ( ( A e. RR+ /\ ( B e. RR+ /\ 1 < B ) ) -> ( B logb A ) = ( ( log ` A ) / ( log ` B ) ) )
13 12 breq2d 
 |-  ( ( A e. RR+ /\ ( B e. RR+ /\ 1 < B ) ) -> ( 0 < ( B logb A ) <-> 0 < ( ( log ` A ) / ( log ` B ) ) ) )
14 relogcl 
 |-  ( A e. RR+ -> ( log ` A ) e. RR )
15 14 adantr 
 |-  ( ( A e. RR+ /\ ( B e. RR+ /\ 1 < B ) ) -> ( log ` A ) e. RR )
16 relogcl 
 |-  ( B e. RR+ -> ( log ` B ) e. RR )
17 16 adantr 
 |-  ( ( B e. RR+ /\ 1 < B ) -> ( log ` B ) e. RR )
18 17 adantl 
 |-  ( ( A e. RR+ /\ ( B e. RR+ /\ 1 < B ) ) -> ( log ` B ) e. RR )
19 loggt0b 
 |-  ( B e. RR+ -> ( 0 < ( log ` B ) <-> 1 < B ) )
20 19 biimpar 
 |-  ( ( B e. RR+ /\ 1 < B ) -> 0 < ( log ` B ) )
21 20 adantl 
 |-  ( ( A e. RR+ /\ ( B e. RR+ /\ 1 < B ) ) -> 0 < ( log ` B ) )
22 gt0div 
 |-  ( ( ( log ` A ) e. RR /\ ( log ` B ) e. RR /\ 0 < ( log ` B ) ) -> ( 0 < ( log ` A ) <-> 0 < ( ( log ` A ) / ( log ` B ) ) ) )
23 15 18 21 22 syl3anc 
 |-  ( ( A e. RR+ /\ ( B e. RR+ /\ 1 < B ) ) -> ( 0 < ( log ` A ) <-> 0 < ( ( log ` A ) / ( log ` B ) ) ) )
24 loggt0b 
 |-  ( A e. RR+ -> ( 0 < ( log ` A ) <-> 1 < A ) )
25 24 adantr 
 |-  ( ( A e. RR+ /\ ( B e. RR+ /\ 1 < B ) ) -> ( 0 < ( log ` A ) <-> 1 < A ) )
26 13 23 25 3bitr2d 
 |-  ( ( A e. RR+ /\ ( B e. RR+ /\ 1 < B ) ) -> ( 0 < ( B logb A ) <-> 1 < A ) )