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