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

Metamath Proof Explorer

Theorem logbcl

Description: General logarithm closure. (Contributed by David A. Wheeler, 17-Jul-2017)

Ref Expression
Assertion logbcl ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 logb 𝑋 ) ∈ ℂ )

Proof

Step Hyp Ref Expression
1 logbval ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 logb 𝑋 ) = ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) )
2 eldifsn ⊢ ( 𝑋 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑋 ∈ ℂ ∧ 𝑋 ≠ 0 ) )
3 logcl ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑋 ≠ 0 ) → ( log ‘ 𝑋 ) ∈ ℂ )
4 2 3 sylbi ⊢ ( 𝑋 ∈ ( ℂ ∖ { 0 } ) → ( log ‘ 𝑋 ) ∈ ℂ )
5 4 adantl ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( log ‘ 𝑋 ) ∈ ℂ )
6 eldifi ⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) → 𝐵 ∈ ℂ )
7 eldifpr ⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ↔ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
8 7 simp2bi ⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) → 𝐵 ≠ 0 )
9 6 8 logcld ⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) → ( log ‘ 𝐵 ) ∈ ℂ )
10 9 adantr ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( log ‘ 𝐵 ) ∈ ℂ )
11 logccne0 ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( log ‘ 𝐵 ) ≠ 0 )
12 7 11 sylbi ⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) → ( log ‘ 𝐵 ) ≠ 0 )
13 12 adantr ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( log ‘ 𝐵 ) ≠ 0 )
14 5 10 13 divcld ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) ∈ ℂ )
15 1 14 eqeltrd ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 logb 𝑋 ) ∈ ℂ )