Theorem relogbzcl

Description: Closure of the general logarithm with integer base on positive reals. (Contributed by Thierry Arnoux, 27-Sep-2017) (Proof shortened by AV, 9-Jun-2020)

	Ref	Expression
Assertion	relogbzcl	⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → ( 𝐵 logb 𝑋 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		zgt1rpn0n1	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
2		relogbcl	⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝑋 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) → ( 𝐵 logb 𝑋 ) ∈ ℝ )
3	2	3com23	⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ∧ 𝑋 ∈ ℝ+ ) → ( 𝐵 logb 𝑋 ) ∈ ℝ )
4	3	3expia	⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) → ( 𝑋 ∈ ℝ+ → ( 𝐵 logb 𝑋 ) ∈ ℝ ) )
5	4	3adant2	⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( 𝑋 ∈ ℝ+ → ( 𝐵 logb 𝑋 ) ∈ ℝ ) )
6	1 5	syl	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑋 ∈ ℝ+ → ( 𝐵 logb 𝑋 ) ∈ ℝ ) )
7	6	imp	⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → ( 𝐵 logb 𝑋 ) ∈ ℝ )