Theorem relogbcld

Description: Closure of the general logarithm with a positive real base on positive reals, a deduction version. (Contributed by metakunt, 22-May-2024)

	Ref	Expression
Hypotheses	relogbcld.1	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	relogbcld.2	⊢ ( 𝜑 → 0 < 𝐵 )
	relogbcld.3	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
	relogbcld.4	⊢ ( 𝜑 → 0 < 𝑋 )
	relogbcld.5	⊢ ( 𝜑 → 𝐵 ≠ 1 )
Assertion	relogbcld	⊢ ( 𝜑 → ( 𝐵 logb 𝑋 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		relogbcld.1	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
2		relogbcld.2	⊢ ( 𝜑 → 0 < 𝐵 )
3		relogbcld.3	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
4		relogbcld.4	⊢ ( 𝜑 → 0 < 𝑋 )
5		relogbcld.5	⊢ ( 𝜑 → 𝐵 ≠ 1 )
6	1 2	elrpd	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
7	3 4	elrpd	⊢ ( 𝜑 → 𝑋 ∈ ℝ+ )
8	6 7 5	3jca	⊢ ( 𝜑 → ( 𝐵 ∈ ℝ+ ∧ 𝑋 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) )
9		relogbcl	⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝑋 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) → ( 𝐵 logb 𝑋 ) ∈ ℝ )
10	8 9	syl	⊢ ( 𝜑 → ( 𝐵 logb 𝑋 ) ∈ ℝ )