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

Metamath Proof Explorer

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	$⊢ (B \in ℤ_{\geq 2} \land X \in ℝ^{+}) \to \log_{B} X \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		zgt1rpn0n1	$⊢ B \in ℤ_{\geq 2} \to (B \in ℝ^{+} \land B \neq 0 \land B \neq 1)$
2		relogbcl	$⊢ (B \in ℝ^{+} \land X \in ℝ^{+} \land B \neq 1) \to \log_{B} X \in ℝ$
3	2	3com23	$⊢ (B \in ℝ^{+} \land B \neq 1 \land X \in ℝ^{+}) \to \log_{B} X \in ℝ$
4	3	3expia	$⊢ (B \in ℝ^{+} \land B \neq 1) \to (X \in ℝ^{+} \to \log_{B} X \in ℝ)$
5	4	3adant2	$⊢ (B \in ℝ^{+} \land B \neq 0 \land B \neq 1) \to (X \in ℝ^{+} \to \log_{B} X \in ℝ)$
6	1 5	syl	$⊢ B \in ℤ_{\geq 2} \to (X \in ℝ^{+} \to \log_{B} X \in ℝ)$
7	6	imp	$⊢ (B \in ℤ_{\geq 2} \land X \in ℝ^{+}) \to \log_{B} X \in ℝ$