# 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 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {X}\in {ℝ}^{+}\right)\to {\mathrm{log}}_{{B}}{X}\in ℝ$

### Proof

Step Hyp Ref Expression
1 zgt1rpn0n1 ${⊢}{B}\in {ℤ}_{\ge 2}\to \left({B}\in {ℝ}^{+}\wedge {B}\ne 0\wedge {B}\ne 1\right)$
2 relogbcl ${⊢}\left({B}\in {ℝ}^{+}\wedge {X}\in {ℝ}^{+}\wedge {B}\ne 1\right)\to {\mathrm{log}}_{{B}}{X}\in ℝ$
3 2 3com23 ${⊢}\left({B}\in {ℝ}^{+}\wedge {B}\ne 1\wedge {X}\in {ℝ}^{+}\right)\to {\mathrm{log}}_{{B}}{X}\in ℝ$
4 3 3expia ${⊢}\left({B}\in {ℝ}^{+}\wedge {B}\ne 1\right)\to \left({X}\in {ℝ}^{+}\to {\mathrm{log}}_{{B}}{X}\in ℝ\right)$
5 4 3adant2 ${⊢}\left({B}\in {ℝ}^{+}\wedge {B}\ne 0\wedge {B}\ne 1\right)\to \left({X}\in {ℝ}^{+}\to {\mathrm{log}}_{{B}}{X}\in ℝ\right)$
6 1 5 syl ${⊢}{B}\in {ℤ}_{\ge 2}\to \left({X}\in {ℝ}^{+}\to {\mathrm{log}}_{{B}}{X}\in ℝ\right)$
7 6 imp ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {X}\in {ℝ}^{+}\right)\to {\mathrm{log}}_{{B}}{X}\in ℝ$