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	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) → ( ( log ‘ 𝐴 ) / ( log ‘ 𝐵 ) ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		relogcl	⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℝ )
2	1	3ad2ant1	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) → ( log ‘ 𝐴 ) ∈ ℝ )
3		relogcl	⊢ ( 𝐵 ∈ ℝ+ → ( log ‘ 𝐵 ) ∈ ℝ )
4	3	3ad2ant2	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) → ( log ‘ 𝐵 ) ∈ ℝ )
5		logne0	⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) → ( log ‘ 𝐵 ) ≠ 0 )
6	5	3adant1	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) → ( log ‘ 𝐵 ) ≠ 0 )
7	2 4 6	redivcld	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) → ( ( log ‘ 𝐴 ) / ( log ‘ 𝐵 ) ) ∈ ℝ )