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 ( ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) → ( ( curry logb𝐵 ) ↾ ℝ+ ) : ℝ+ ⟶ ℝ )

Proof

Step Hyp Ref Expression
1 rpcndif0 ( 𝑥 ∈ ℝ+𝑥 ∈ ( ℂ ∖ { 0 } ) )
2 1 adantl ( ( ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ( ℂ ∖ { 0 } ) )
3 rpcn ( 𝐵 ∈ ℝ+𝐵 ∈ ℂ )
4 3 adantr ( ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) → 𝐵 ∈ ℂ )
5 rpne0 ( 𝐵 ∈ ℝ+𝐵 ≠ 0 )
6 5 adantr ( ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) → 𝐵 ≠ 0 )
7 animorr ( ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) → ( 𝐵 < 1 ∨ 1 < 𝐵 ) )
8 rpre ( 𝐵 ∈ ℝ+𝐵 ∈ ℝ )
9 1red ( 1 < 𝐵 → 1 ∈ ℝ )
10 lttri2 ( ( 𝐵 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝐵 ≠ 1 ↔ ( 𝐵 < 1 ∨ 1 < 𝐵 ) ) )
11 8 9 10 syl2an ( ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) → ( 𝐵 ≠ 1 ↔ ( 𝐵 < 1 ∨ 1 < 𝐵 ) ) )
12 7 11 mpbird ( ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) → 𝐵 ≠ 1 )
13 4 6 12 3jca ( ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
14 logbmpt ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( curry logb𝐵 ) = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( ( log ‘ 𝑥 ) / ( log ‘ 𝐵 ) ) ) )
15 13 14 syl ( ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) → ( curry logb𝐵 ) = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( ( log ‘ 𝑥 ) / ( log ‘ 𝐵 ) ) ) )
16 15 dmeqd ( ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) → dom ( curry logb𝐵 ) = dom ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( ( log ‘ 𝑥 ) / ( log ‘ 𝐵 ) ) ) )
17 ovexd ( ( ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( ( log ‘ 𝑥 ) / ( log ‘ 𝐵 ) ) ∈ V )
18 17 ralrimiva ( ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) → ∀ 𝑥 ∈ ( ℂ ∖ { 0 } ) ( ( log ‘ 𝑥 ) / ( log ‘ 𝐵 ) ) ∈ V )
19 dmmptg ( ∀ 𝑥 ∈ ( ℂ ∖ { 0 } ) ( ( log ‘ 𝑥 ) / ( log ‘ 𝐵 ) ) ∈ V → dom ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( ( log ‘ 𝑥 ) / ( log ‘ 𝐵 ) ) ) = ( ℂ ∖ { 0 } ) )
20 18 19 syl ( ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) → dom ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( ( log ‘ 𝑥 ) / ( log ‘ 𝐵 ) ) ) = ( ℂ ∖ { 0 } ) )
21 16 20 eqtrd ( ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) → dom ( curry logb𝐵 ) = ( ℂ ∖ { 0 } ) )
22 21 adantr ( ( ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) ∧ 𝑥 ∈ ℝ+ ) → dom ( curry logb𝐵 ) = ( ℂ ∖ { 0 } ) )
23 2 22 eleqtrrd ( ( ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ dom ( curry logb𝐵 ) )
24 logbfval ( ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( ( curry logb𝐵 ) ‘ 𝑥 ) = ( 𝐵 logb 𝑥 ) )
25 13 1 24 syl2an ( ( ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( curry logb𝐵 ) ‘ 𝑥 ) = ( 𝐵 logb 𝑥 ) )
26 simpll ( ( ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) ∧ 𝑥 ∈ ℝ+ ) → 𝐵 ∈ ℝ+ )
27 simpr ( ( ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
28 12 adantr ( ( ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) ∧ 𝑥 ∈ ℝ+ ) → 𝐵 ≠ 1 )
29 26 27 28 3jca ( ( ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐵 ∈ ℝ+𝑥 ∈ ℝ+𝐵 ≠ 1 ) )
30 relogbcl ( ( 𝐵 ∈ ℝ+𝑥 ∈ ℝ+𝐵 ≠ 1 ) → ( 𝐵 logb 𝑥 ) ∈ ℝ )
31 29 30 syl ( ( ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐵 logb 𝑥 ) ∈ ℝ )
32 25 31 eqeltrd ( ( ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( curry logb𝐵 ) ‘ 𝑥 ) ∈ ℝ )
33 23 32 jca ( ( ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ∈ dom ( curry logb𝐵 ) ∧ ( ( curry logb𝐵 ) ‘ 𝑥 ) ∈ ℝ ) )
34 33 ralrimiva ( ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) → ∀ 𝑥 ∈ ℝ+ ( 𝑥 ∈ dom ( curry logb𝐵 ) ∧ ( ( curry logb𝐵 ) ‘ 𝑥 ) ∈ ℝ ) )
35 logbf ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( curry logb𝐵 ) : ( ℂ ∖ { 0 } ) ⟶ ℂ )
36 13 35 syl ( ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) → ( curry logb𝐵 ) : ( ℂ ∖ { 0 } ) ⟶ ℂ )
37 ffun ( ( curry logb𝐵 ) : ( ℂ ∖ { 0 } ) ⟶ ℂ → Fun ( curry logb𝐵 ) )
38 ffvresb ( Fun ( curry logb𝐵 ) → ( ( ( curry logb𝐵 ) ↾ ℝ+ ) : ℝ+ ⟶ ℝ ↔ ∀ 𝑥 ∈ ℝ+ ( 𝑥 ∈ dom ( curry logb𝐵 ) ∧ ( ( curry logb𝐵 ) ‘ 𝑥 ) ∈ ℝ ) ) )
39 36 37 38 3syl ( ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) → ( ( ( curry logb𝐵 ) ↾ ℝ+ ) : ℝ+ ⟶ ℝ ↔ ∀ 𝑥 ∈ ℝ+ ( 𝑥 ∈ dom ( curry logb𝐵 ) ∧ ( ( curry logb𝐵 ) ‘ 𝑥 ) ∈ ℝ ) ) )
40 34 39 mpbird ( ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) → ( ( curry logb𝐵 ) ↾ ℝ+ ) : ℝ+ ⟶ ℝ )