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

Metamath Proof Explorer

Theorem logbfval

Description: The general logarithm of a complex number to a fixed base. (Contributed by AV, 11-Jun-2020)

Ref Expression
Assertion logbfval ( ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( ( curry logb ‘ 𝐵 ) ‘ 𝑋 ) = ( 𝐵 logb 𝑋 ) )

Proof

Step Hyp Ref Expression
1 df-logb ⊢ logb = ( 𝑥 ∈ ( ℂ ∖ { 0 , 1 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ( log ‘ 𝑦 ) / ( log ‘ 𝑥 ) ) )
2 ovexd ⊢ ( ( ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑥 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ) → ( ( log ‘ 𝑦 ) / ( log ‘ 𝑥 ) ) ∈ V )
3 2 ralrimivva ⊢ ( ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ∀ 𝑥 ∈ ( ℂ ∖ { 0 , 1 } ) ∀ 𝑦 ∈ ( ℂ ∖ { 0 } ) ( ( log ‘ 𝑦 ) / ( log ‘ 𝑥 ) ) ∈ V )
4 cnex ⊢ ℂ ∈ V
5 difexg ⊢ ( ℂ ∈ V → ( ℂ ∖ { 0 } ) ∈ V )
6 4 5 mp1i ⊢ ( ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( ℂ ∖ { 0 } ) ∈ V )
7 eldifpr ⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ↔ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
8 7 biimpri ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) )
9 8 adantr ⊢ ( ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) )
10 simpr ⊢ ( ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → 𝑋 ∈ ( ℂ ∖ { 0 } ) )
11 1 3 6 9 10 fvmpocurryd ⊢ ( ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( ( curry logb ‘ 𝐵 ) ‘ 𝑋 ) = ( 𝐵 logb 𝑋 ) )