Metamath Proof Explorer

Theorem logblt1b

Description: The logarithm of a number is less than 1 iff the number is less than the base of the logarithm. (Contributed by AV, 30-May-2020)

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

Proof

Step Hyp Ref Expression
1 relogbval 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ ) -> ( B logb X ) = ( ( log ` X ) / ( log ` B ) ) )
2 1 breq1d 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ ) -> ( ( B logb X ) < 1 <-> ( ( log ` X ) / ( log ` B ) ) < 1 ) )
3 relogcl 
 |-  ( X e. RR+ -> ( log ` X ) e. RR )
4 3 adantl 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ ) -> ( log ` X ) e. RR )
5 1red 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ ) -> 1 e. RR )
6 eluz2nn 
 |-  ( B e. ( ZZ>= ` 2 ) -> B e. NN )
7 6 nnrpd 
 |-  ( B e. ( ZZ>= ` 2 ) -> B e. RR+ )
8 relogcl 
 |-  ( B e. RR+ -> ( log ` B ) e. RR )
9 7 8 syl 
 |-  ( B e. ( ZZ>= ` 2 ) -> ( log ` B ) e. RR )
10 eluz2gt1 
 |-  ( B e. ( ZZ>= ` 2 ) -> 1 < B )
11 loggt0b 
 |-  ( B e. RR+ -> ( 0 < ( log ` B ) <-> 1 < B ) )
12 7 11 syl 
 |-  ( B e. ( ZZ>= ` 2 ) -> ( 0 < ( log ` B ) <-> 1 < B ) )
13 10 12 mpbird 
 |-  ( B e. ( ZZ>= ` 2 ) -> 0 < ( log ` B ) )
14 9 13 jca 
 |-  ( B e. ( ZZ>= ` 2 ) -> ( ( log ` B ) e. RR /\ 0 < ( log ` B ) ) )
15 14 adantr 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ ) -> ( ( log ` B ) e. RR /\ 0 < ( log ` B ) ) )
16 ltdivmul 
 |-  ( ( ( log ` X ) e. RR /\ 1 e. RR /\ ( ( log ` B ) e. RR /\ 0 < ( log ` B ) ) ) -> ( ( ( log ` X ) / ( log ` B ) ) < 1 <-> ( log ` X ) < ( ( log ` B ) x. 1 ) ) )
17 4 5 15 16 syl3anc 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ ) -> ( ( ( log ` X ) / ( log ` B ) ) < 1 <-> ( log ` X ) < ( ( log ` B ) x. 1 ) ) )
18 9 recnd 
 |-  ( B e. ( ZZ>= ` 2 ) -> ( log ` B ) e. CC )
19 18 mulridd 
 |-  ( B e. ( ZZ>= ` 2 ) -> ( ( log ` B ) x. 1 ) = ( log ` B ) )
20 19 adantr 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ ) -> ( ( log ` B ) x. 1 ) = ( log ` B ) )
21 20 breq2d 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ ) -> ( ( log ` X ) < ( ( log ` B ) x. 1 ) <-> ( log ` X ) < ( log ` B ) ) )
22 7 anim2i 
 |-  ( ( X e. RR+ /\ B e. ( ZZ>= ` 2 ) ) -> ( X e. RR+ /\ B e. RR+ ) )
23 22 ancoms 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ ) -> ( X e. RR+ /\ B e. RR+ ) )
24 logltb 
 |-  ( ( X e. RR+ /\ B e. RR+ ) -> ( X < B <-> ( log ` X ) < ( log ` B ) ) )
25 24 bicomd 
 |-  ( ( X e. RR+ /\ B e. RR+ ) -> ( ( log ` X ) < ( log ` B ) <-> X < B ) )
26 23 25 syl 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ ) -> ( ( log ` X ) < ( log ` B ) <-> X < B ) )
27 21 26 bitrd 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ ) -> ( ( log ` X ) < ( ( log ` B ) x. 1 ) <-> X < B ) )
28 17 27 bitrd 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ ) -> ( ( ( log ` X ) / ( log ` B ) ) < 1 <-> X < B ) )
29 2 28 bitrd 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ ) -> ( ( B logb X ) < 1 <-> X < B ) )