Theorem reglogcl

Description: General logarithm is a real number. (Contributed by Stefan O'Rear, 19-Sep-2014) (New usage is discouraged.) Use relogbcl instead.

	Ref	Expression
Assertion	reglogcl	$$⊢\left(A\in {ℝ}^{+}\wedge B\in {ℝ}^{+}\wedge B\ne 1\right)\to \frac{\log A}{\log B}\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		relogcl	$$⊢A\in {ℝ}^{+}\to \log A\in ℝ$$
2	1	3ad2ant1	$$⊢\left(A\in {ℝ}^{+}\wedge B\in {ℝ}^{+}\wedge B\ne 1\right)\to \log A\in ℝ$$
3		relogcl	$$⊢B\in {ℝ}^{+}\to \log B\in ℝ$$
4	3	3ad2ant2	$$⊢\left(A\in {ℝ}^{+}\wedge B\in {ℝ}^{+}\wedge B\ne 1\right)\to \log B\in ℝ$$
5		logne0	$$⊢\left(B\in {ℝ}^{+}\wedge B\ne 1\right)\to \log B\ne 0$$
6	5	3adant1	$$⊢\left(A\in {ℝ}^{+}\wedge B\in {ℝ}^{+}\wedge B\ne 1\right)\to \log B\ne 0$$
7	2 4 6	redivcld	$$⊢\left(A\in {ℝ}^{+}\wedge B\in {ℝ}^{+}\wedge B\ne 1\right)\to \frac{\log A}{\log B}\in ℝ$$