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	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to {\log }_{B}X\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		zgt1rpn0n1	$$⊢B\in {\mathbb{Z}}_{\ge 2}\to \left(B\in {ℝ}^{+}\wedge B\ne 0\wedge B\ne 1\right)$$
2		relogbcl	$$⊢\left(B\in {ℝ}^{+}\wedge X\in {ℝ}^{+}\wedge B\ne 1\right)\to {\log }_{B}X\in ℝ$$
3	2	3com23	$$⊢\left(B\in {ℝ}^{+}\wedge B\ne 1\wedge X\in {ℝ}^{+}\right)\to {\log }_{B}X\in ℝ$$
4	3	3expia	$$⊢\left(B\in {ℝ}^{+}\wedge B\ne 1\right)\to \left(X\in {ℝ}^{+}\to {\log }_{B}X\in ℝ\right)$$
5	4	3adant2	$$⊢\left(B\in {ℝ}^{+}\wedge B\ne 0\wedge B\ne 1\right)\to \left(X\in {ℝ}^{+}\to {\log }_{B}X\in ℝ\right)$$
6	1 5	syl	$$⊢B\in {\mathbb{Z}}_{\ge 2}\to \left(X\in {ℝ}^{+}\to {\log }_{B}X\in ℝ\right)$$
7	6	imp	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to {\log }_{B}X\in ℝ$$