This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem relogbval

Description: Value of the general logarithm with integer base. (Contributed by Thierry Arnoux, 27-Sep-2017)

Ref Expression
Assertion relogbval ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → ( 𝐵 logb 𝑋 ) = ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 zgt1rpn0n1 ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
2 1 adantr ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
3 2 simp1d ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → 𝐵 ∈ ℝ+ )
4 3 rpcnd ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → 𝐵 ∈ ℂ )
5 2 simp2d ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → 𝐵 ≠ 0 )
6 2 simp3d ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → 𝐵 ≠ 1 )
7 eldifpr ⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ↔ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
8 4 5 6 7 syl3anbrc ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) )
9 simpr ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → 𝑋 ∈ ℝ+ )
10 9 rpcnne0d ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → ( 𝑋 ∈ ℂ ∧ 𝑋 ≠ 0 ) )
11 eldifsn ⊢ ( 𝑋 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑋 ∈ ℂ ∧ 𝑋 ≠ 0 ) )
12 10 11 sylibr ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → 𝑋 ∈ ( ℂ ∖ { 0 } ) )
13 logbval ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 logb 𝑋 ) = ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) )
14 8 12 13 syl2anc ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → ( 𝐵 logb 𝑋 ) = ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) )