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 ffun 
 |-  ( ( curry logb ` B ) : ( CC \ { 0 } ) --> CC -> Fun ( curry logb ` B ) )
37 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 ) ) )
38 13 35 36 37 4syl 
 |-  ( ( 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 ) ) )
39 34 38 mpbird 
 |-  ( ( B e. RR+ /\ 1 < B ) -> ( ( curry logb ` B ) |` RR+ ) : RR+ --> RR )