Metamath Proof Explorer


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 ‘ 𝐵 ) ) ∈ ℝ )