relogbcl

Description: Closure of the general logarithm with a positive real base on positive reals. (Contributed by Stefan O'Rear, 19-Sep-2014) (Revised by Thierry Arnoux, 27-Sep-2017)

		Ref	Expression
	Assertion	relogbcl	⊢ ( ( 𝐵 ∈ ℝ⁺ ∧ 𝑋 ∈ ℝ⁺ ∧ 𝐵 ≠ 1 ) → ( 𝐵 log_b 𝑋 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝐵 ∈ ℝ⁺ ∧ 𝑋 ∈ ℝ⁺ ∧ 𝐵 ≠ 1 ) → 𝐵 ∈ ℝ⁺ )
2	1	rpcnne0d	⊢ ( ( 𝐵 ∈ ℝ⁺ ∧ 𝑋 ∈ ℝ⁺ ∧ 𝐵 ≠ 1 ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
3		simp3	⊢ ( ( 𝐵 ∈ ℝ⁺ ∧ 𝑋 ∈ ℝ⁺ ∧ 𝐵 ≠ 1 ) → 𝐵 ≠ 1 )
4		df-3an	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) ↔ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐵 ≠ 1 ) )
5	2 3 4	sylanbrc	⊢ ( ( 𝐵 ∈ ℝ⁺ ∧ 𝑋 ∈ ℝ⁺ ∧ 𝐵 ≠ 1 ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
6		eldifpr	⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ↔ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
7	5 6	sylibr	⊢ ( ( 𝐵 ∈ ℝ⁺ ∧ 𝑋 ∈ ℝ⁺ ∧ 𝐵 ≠ 1 ) → 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) )
8		simp2	⊢ ( ( 𝐵 ∈ ℝ⁺ ∧ 𝑋 ∈ ℝ⁺ ∧ 𝐵 ≠ 1 ) → 𝑋 ∈ ℝ⁺ )
9	8	rpcnne0d	⊢ ( ( 𝐵 ∈ ℝ⁺ ∧ 𝑋 ∈ ℝ⁺ ∧ 𝐵 ≠ 1 ) → ( 𝑋 ∈ ℂ ∧ 𝑋 ≠ 0 ) )
10		eldifsn	⊢ ( 𝑋 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑋 ∈ ℂ ∧ 𝑋 ≠ 0 ) )
11	9 10	sylibr	⊢ ( ( 𝐵 ∈ ℝ⁺ ∧ 𝑋 ∈ ℝ⁺ ∧ 𝐵 ≠ 1 ) → 𝑋 ∈ ( ℂ ∖ { 0 } ) )
12		logbval	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 log_b 𝑋 ) = ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) )
13	7 11 12	syl2anc	⊢ ( ( 𝐵 ∈ ℝ⁺ ∧ 𝑋 ∈ ℝ⁺ ∧ 𝐵 ≠ 1 ) → ( 𝐵 log_b 𝑋 ) = ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) )
14		relogcl	⊢ ( 𝑋 ∈ ℝ⁺ → ( log ‘ 𝑋 ) ∈ ℝ )
15	14	3ad2ant2	⊢ ( ( 𝐵 ∈ ℝ⁺ ∧ 𝑋 ∈ ℝ⁺ ∧ 𝐵 ≠ 1 ) → ( log ‘ 𝑋 ) ∈ ℝ )
16		relogcl	⊢ ( 𝐵 ∈ ℝ⁺ → ( log ‘ 𝐵 ) ∈ ℝ )
17	16	3ad2ant1	⊢ ( ( 𝐵 ∈ ℝ⁺ ∧ 𝑋 ∈ ℝ⁺ ∧ 𝐵 ≠ 1 ) → ( log ‘ 𝐵 ) ∈ ℝ )
18		logne0	⊢ ( ( 𝐵 ∈ ℝ⁺ ∧ 𝐵 ≠ 1 ) → ( log ‘ 𝐵 ) ≠ 0 )
19	18	3adant2	⊢ ( ( 𝐵 ∈ ℝ⁺ ∧ 𝑋 ∈ ℝ⁺ ∧ 𝐵 ≠ 1 ) → ( log ‘ 𝐵 ) ≠ 0 )
20	15 17 19	redivcld	⊢ ( ( 𝐵 ∈ ℝ⁺ ∧ 𝑋 ∈ ℝ⁺ ∧ 𝐵 ≠ 1 ) → ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) ∈ ℝ )
21	13 20	eqeltrd	⊢ ( ( 𝐵 ∈ ℝ⁺ ∧ 𝑋 ∈ ℝ⁺ ∧ 𝐵 ≠ 1 ) → ( 𝐵 log_b 𝑋 ) ∈ ℝ )

Metamath Proof Explorer

Theorem relogbcl

Proof