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

Metamath Proof Explorer

Theorem logbf

Description: The general logarithm to a fixed base regarded as function. (Contributed by AV, 11-Jun-2020)

Ref Expression
Assertion logbf ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( curry logb ‘ 𝐵 ) : ( ℂ ∖ { 0 } ) ⟶ ℂ )

Proof

Step Hyp Ref Expression
1 logbmpt ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( curry logb ‘ 𝐵 ) = ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ( log ‘ 𝑦 ) / ( log ‘ 𝐵 ) ) ) )
2 eldifsn ⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) )
3 logcl ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) → ( log ‘ 𝑦 ) ∈ ℂ )
4 2 3 sylbi ⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) → ( log ‘ 𝑦 ) ∈ ℂ )
5 4 adantl ⊢ ( ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( log ‘ 𝑦 ) ∈ ℂ )
6 logcl ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( log ‘ 𝐵 ) ∈ ℂ )
7 6 3adant3 ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( log ‘ 𝐵 ) ∈ ℂ )
8 7 adantr ⊢ ( ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( log ‘ 𝐵 ) ∈ ℂ )
9 logccne0 ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( log ‘ 𝐵 ) ≠ 0 )
10 9 adantr ⊢ ( ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( log ‘ 𝐵 ) ≠ 0 )
11 5 8 10 divcld ⊢ ( ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( ( log ‘ 𝑦 ) / ( log ‘ 𝐵 ) ) ∈ ℂ )
12 1 11 fmpt3d ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( curry logb ‘ 𝐵 ) : ( ℂ ∖ { 0 } ) ⟶ ℂ )