Metamath Proof Explorer

Theorem fllogbd

Description: A real number is between the base of a logarithm to the power of the floor of the logarithm of the number and the base of the logarithm to the power of the floor of the logarithm of the number plus one. (Contributed by AV, 23-May-2020)

Ref Expression
Hypotheses fllogbd.b 
|- ( ph -> B e. ( ZZ>= ` 2 ) )
fllogbd.x 
|- ( ph -> X e. RR+ )
fllogbd.e 
|- E = ( |_ ` ( B logb X ) )
Assertion fllogbd 
|- ( ph -> ( ( B ^ E ) <_ X /\ X < ( B ^ ( E + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 fllogbd.b 
 |-  ( ph -> B e. ( ZZ>= ` 2 ) )
2 fllogbd.x 
 |-  ( ph -> X e. RR+ )
3 fllogbd.e 
 |-  E = ( |_ ` ( B logb X ) )
4 relogbzcl 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ ) -> ( B logb X ) e. RR )
5 1 2 4 syl2anc 
 |-  ( ph -> ( B logb X ) e. RR )
6 flle 
 |-  ( ( B logb X ) e. RR -> ( |_ ` ( B logb X ) ) <_ ( B logb X ) )
7 5 6 syl 
 |-  ( ph -> ( |_ ` ( B logb X ) ) <_ ( B logb X ) )
8 3 7 eqbrtrid 
 |-  ( ph -> E <_ ( B logb X ) )
9 eluzelz 
 |-  ( B e. ( ZZ>= ` 2 ) -> B e. ZZ )
10 1 9 syl 
 |-  ( ph -> B e. ZZ )
11 10 zred 
 |-  ( ph -> B e. RR )
12 eluz2b1 
 |-  ( B e. ( ZZ>= ` 2 ) <-> ( B e. ZZ /\ 1 < B ) )
13 12 simprbi 
 |-  ( B e. ( ZZ>= ` 2 ) -> 1 < B )
14 1 13 syl 
 |-  ( ph -> 1 < B )
15 5 flcld 
 |-  ( ph -> ( |_ ` ( B logb X ) ) e. ZZ )
16 3 15 eqeltrid 
 |-  ( ph -> E e. ZZ )
17 16 zred 
 |-  ( ph -> E e. RR )
18 11 14 17 5 cxpled 
 |-  ( ph -> ( E <_ ( B logb X ) <-> ( B ^c E ) <_ ( B ^c ( B logb X ) ) ) )
19 8 18 mpbid 
 |-  ( ph -> ( B ^c E ) <_ ( B ^c ( B logb X ) ) )
20 10 zcnd 
 |-  ( ph -> B e. CC )
21 eluz2nn 
 |-  ( B e. ( ZZ>= ` 2 ) -> B e. NN )
22 1 21 syl 
 |-  ( ph -> B e. NN )
23 22 nnne0d 
 |-  ( ph -> B =/= 0 )
24 20 23 16 cxpexpzd 
 |-  ( ph -> ( B ^c E ) = ( B ^ E ) )
25 eluz2cnn0n1 
 |-  ( B e. ( ZZ>= ` 2 ) -> B e. ( CC \ { 0 , 1 } ) )
26 1 25 syl 
 |-  ( ph -> B e. ( CC \ { 0 , 1 } ) )
27 rpcnne0 
 |-  ( X e. RR+ -> ( X e. CC /\ X =/= 0 ) )
28 eldifsn 
 |-  ( X e. ( CC \ { 0 } ) <-> ( X e. CC /\ X =/= 0 ) )
29 27 28 sylibr 
 |-  ( X e. RR+ -> X e. ( CC \ { 0 } ) )
30 2 29 syl 
 |-  ( ph -> X e. ( CC \ { 0 } ) )
31 cxplogb 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( B ^c ( B logb X ) ) = X )
32 26 30 31 syl2anc 
 |-  ( ph -> ( B ^c ( B logb X ) ) = X )
33 19 24 32 3brtr3d 
 |-  ( ph -> ( B ^ E ) <_ X )
34 flltp1 
 |-  ( ( B logb X ) e. RR -> ( B logb X ) < ( ( |_ ` ( B logb X ) ) + 1 ) )
35 5 34 syl 
 |-  ( ph -> ( B logb X ) < ( ( |_ ` ( B logb X ) ) + 1 ) )
36 3 a1i 
 |-  ( ph -> E = ( |_ ` ( B logb X ) ) )
37 36 oveq1d 
 |-  ( ph -> ( E + 1 ) = ( ( |_ ` ( B logb X ) ) + 1 ) )
38 35 37 breqtrrd 
 |-  ( ph -> ( B logb X ) < ( E + 1 ) )
39 16 peano2zd 
 |-  ( ph -> ( E + 1 ) e. ZZ )
40 39 zred 
 |-  ( ph -> ( E + 1 ) e. RR )
41 11 14 5 40 cxpltd 
 |-  ( ph -> ( ( B logb X ) < ( E + 1 ) <-> ( B ^c ( B logb X ) ) < ( B ^c ( E + 1 ) ) ) )
42 38 41 mpbid 
 |-  ( ph -> ( B ^c ( B logb X ) ) < ( B ^c ( E + 1 ) ) )
43 20 23 39 cxpexpzd 
 |-  ( ph -> ( B ^c ( E + 1 ) ) = ( B ^ ( E + 1 ) ) )
44 42 32 43 3brtr3d 
 |-  ( ph -> X < ( B ^ ( E + 1 ) ) )
45 33 44 jca 
 |-  ( ph -> ( ( B ^ E ) <_ X /\ X < ( B ^ ( E + 1 ) ) ) )