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 ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 → curry logb ⁡ B : ℂ ∖ 0 ⟶ ℂ

Proof

Step Hyp Ref Expression
1 logbmpt ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 → curry logb ⁡ B = y ∈ ℂ ∖ 0 ⟼ log ⁡ y log ⁡ B
2 eldifsn ⊢ y ∈ ℂ ∖ 0 ↔ y ∈ ℂ ∧ y ≠ 0
3 logcl ⊢ y ∈ ℂ ∧ y ≠ 0 → log ⁡ y ∈ ℂ
4 2 3 sylbi ⊢ y ∈ ℂ ∖ 0 → log ⁡ y ∈ ℂ
5 4 adantl ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 ∧ y ∈ ℂ ∖ 0 → log ⁡ y ∈ ℂ
6 logcl ⊢ B ∈ ℂ ∧ B ≠ 0 → log ⁡ B ∈ ℂ
7 6 3adant3 ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 → log ⁡ B ∈ ℂ
8 7 adantr ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 ∧ y ∈ ℂ ∖ 0 → log ⁡ B ∈ ℂ
9 logccne0 ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 → log ⁡ B ≠ 0
10 9 adantr ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 ∧ y ∈ ℂ ∖ 0 → log ⁡ B ≠ 0
11 5 8 10 divcld ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 ∧ y ∈ ℂ ∖ 0 → log ⁡ y log ⁡ B ∈ ℂ
12 1 11 fmpt3d ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 → curry logb ⁡ B : ℂ ∖ 0 ⟶ ℂ