Metamath Proof Explorer


Theorem relogbf

Description: The general logarithm to a real base greater than 1 regarded as function restricted to the positive integers. Property in Cohen4 p. 349. (Contributed by AV, 12-Jun-2020)

Ref Expression
Assertion relogbf
|- ( ( B e. RR+ /\ 1 < B ) -> ( ( curry logb ` B ) |` RR+ ) : RR+ --> RR )

Proof

Step Hyp Ref Expression
1 rpcndif0
 |-  ( x e. RR+ -> x e. ( CC \ { 0 } ) )
2 1 adantl
 |-  ( ( ( B e. RR+ /\ 1 < B ) /\ x e. RR+ ) -> x e. ( CC \ { 0 } ) )
3 rpcn
 |-  ( B e. RR+ -> B e. CC )
4 3 adantr
 |-  ( ( B e. RR+ /\ 1 < B ) -> B e. CC )
5 rpne0
 |-  ( B e. RR+ -> B =/= 0 )
6 5 adantr
 |-  ( ( B e. RR+ /\ 1 < B ) -> B =/= 0 )
7 animorr
 |-  ( ( B e. RR+ /\ 1 < B ) -> ( B < 1 \/ 1 < B ) )
8 rpre
 |-  ( B e. RR+ -> B e. RR )
9 1red
 |-  ( 1 < B -> 1 e. RR )
10 lttri2
 |-  ( ( B e. RR /\ 1 e. RR ) -> ( B =/= 1 <-> ( B < 1 \/ 1 < B ) ) )
11 8 9 10 syl2an
 |-  ( ( B e. RR+ /\ 1 < B ) -> ( B =/= 1 <-> ( B < 1 \/ 1 < B ) ) )
12 7 11 mpbird
 |-  ( ( B e. RR+ /\ 1 < B ) -> B =/= 1 )
13 4 6 12 3jca
 |-  ( ( B e. RR+ /\ 1 < B ) -> ( B e. CC /\ B =/= 0 /\ B =/= 1 ) )
14 logbmpt
 |-  ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( curry logb ` B ) = ( x e. ( CC \ { 0 } ) |-> ( ( log ` x ) / ( log ` B ) ) ) )
15 13 14 syl
 |-  ( ( B e. RR+ /\ 1 < B ) -> ( curry logb ` B ) = ( x e. ( CC \ { 0 } ) |-> ( ( log ` x ) / ( log ` B ) ) ) )
16 15 dmeqd
 |-  ( ( B e. RR+ /\ 1 < B ) -> dom ( curry logb ` B ) = dom ( x e. ( CC \ { 0 } ) |-> ( ( log ` x ) / ( log ` B ) ) ) )
17 ovexd
 |-  ( ( ( B e. RR+ /\ 1 < B ) /\ x e. ( CC \ { 0 } ) ) -> ( ( log ` x ) / ( log ` B ) ) e. _V )
18 17 ralrimiva
 |-  ( ( B e. RR+ /\ 1 < B ) -> A. x e. ( CC \ { 0 } ) ( ( log ` x ) / ( log ` B ) ) e. _V )
19 dmmptg
 |-  ( A. x e. ( CC \ { 0 } ) ( ( log ` x ) / ( log ` B ) ) e. _V -> dom ( x e. ( CC \ { 0 } ) |-> ( ( log ` x ) / ( log ` B ) ) ) = ( CC \ { 0 } ) )
20 18 19 syl
 |-  ( ( B e. RR+ /\ 1 < B ) -> dom ( x e. ( CC \ { 0 } ) |-> ( ( log ` x ) / ( log ` B ) ) ) = ( CC \ { 0 } ) )
21 16 20 eqtrd
 |-  ( ( B e. RR+ /\ 1 < B ) -> dom ( curry logb ` B ) = ( CC \ { 0 } ) )
22 21 adantr
 |-  ( ( ( B e. RR+ /\ 1 < B ) /\ x e. RR+ ) -> dom ( curry logb ` B ) = ( CC \ { 0 } ) )
23 2 22 eleqtrrd
 |-  ( ( ( B e. RR+ /\ 1 < B ) /\ x e. RR+ ) -> x e. dom ( curry logb ` B ) )
24 logbfval
 |-  ( ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) /\ x e. ( CC \ { 0 } ) ) -> ( ( curry logb ` B ) ` x ) = ( B logb x ) )
25 13 1 24 syl2an
 |-  ( ( ( B e. RR+ /\ 1 < B ) /\ x e. RR+ ) -> ( ( curry logb ` B ) ` x ) = ( B logb x ) )
26 simpll
 |-  ( ( ( B e. RR+ /\ 1 < B ) /\ x e. RR+ ) -> B e. RR+ )
27 simpr
 |-  ( ( ( B e. RR+ /\ 1 < B ) /\ x e. RR+ ) -> x e. RR+ )
28 12 adantr
 |-  ( ( ( B e. RR+ /\ 1 < B ) /\ x e. RR+ ) -> B =/= 1 )
29 26 27 28 3jca
 |-  ( ( ( B e. RR+ /\ 1 < B ) /\ x e. RR+ ) -> ( B e. RR+ /\ x e. RR+ /\ B =/= 1 ) )
30 relogbcl
 |-  ( ( B e. RR+ /\ x e. RR+ /\ B =/= 1 ) -> ( B logb x ) e. RR )
31 29 30 syl
 |-  ( ( ( B e. RR+ /\ 1 < B ) /\ x e. RR+ ) -> ( B logb x ) e. RR )
32 25 31 eqeltrd
 |-  ( ( ( B e. RR+ /\ 1 < B ) /\ x e. RR+ ) -> ( ( curry logb ` B ) ` x ) e. RR )
33 23 32 jca
 |-  ( ( ( B e. RR+ /\ 1 < B ) /\ x e. RR+ ) -> ( x e. dom ( curry logb ` B ) /\ ( ( curry logb ` B ) ` x ) e. RR ) )
34 33 ralrimiva
 |-  ( ( B e. RR+ /\ 1 < B ) -> A. x e. RR+ ( x e. dom ( curry logb ` B ) /\ ( ( curry logb ` B ) ` x ) e. RR ) )
35 logbf
 |-  ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( curry logb ` B ) : ( CC \ { 0 } ) --> CC )
36 13 35 syl
 |-  ( ( B e. RR+ /\ 1 < B ) -> ( curry logb ` B ) : ( CC \ { 0 } ) --> CC )
37 ffun
 |-  ( ( curry logb ` B ) : ( CC \ { 0 } ) --> CC -> Fun ( curry logb ` B ) )
38 ffvresb
 |-  ( Fun ( curry logb ` B ) -> ( ( ( curry logb ` B ) |` RR+ ) : RR+ --> RR <-> A. x e. RR+ ( x e. dom ( curry logb ` B ) /\ ( ( curry logb ` B ) ` x ) e. RR ) ) )
39 36 37 38 3syl
 |-  ( ( B e. RR+ /\ 1 < B ) -> ( ( ( curry logb ` B ) |` RR+ ) : RR+ --> RR <-> A. x e. RR+ ( x e. dom ( curry logb ` B ) /\ ( ( curry logb ` B ) ` x ) e. RR ) ) )
40 34 39 mpbird
 |-  ( ( B e. RR+ /\ 1 < B ) -> ( ( curry logb ` B ) |` RR+ ) : RR+ --> RR )