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 ‘ 𝐵 ) ↾ ℝ+ ) : ℝ+ ⟶ ℝ )