This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffun ⊢ ( ( curry logb ‘ 𝐵 ) : ( ℂ ∖ { 0 } ) ⟶ ℂ → Fun ( curry logb ‘ 𝐵 ) )
37 ffvresb ⊢ ( Fun ( curry logb ‘ 𝐵 ) → ( ( ( curry logb ‘ 𝐵 ) ↾ ℝ+ ) : ℝ+ ⟶ ℝ ↔ ∀ 𝑥 ∈ ℝ+ ( 𝑥 ∈ dom ( curry logb ‘ 𝐵 ) ∧ ( ( curry logb ‘ 𝐵 ) ‘ 𝑥 ) ∈ ℝ ) ) )
38 13 35 36 37 4syl ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) → ( ( ( curry logb ‘ 𝐵 ) ↾ ℝ+ ) : ℝ+ ⟶ ℝ ↔ ∀ 𝑥 ∈ ℝ+ ( 𝑥 ∈ dom ( curry logb ‘ 𝐵 ) ∧ ( ( curry logb ‘ 𝐵 ) ‘ 𝑥 ) ∈ ℝ ) ) )
39 34 38 mpbird ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) → ( ( curry logb ‘ 𝐵 ) ↾ ℝ+ ) : ℝ+ ⟶ ℝ )