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

Proof

Step Hyp Ref Expression
1 df-logb ⊢ logb = x ∈ ℂ ∖ 0 1 , y ∈ ℂ ∖ 0 ⟼ log ⁡ y log ⁡ x
2 ovexd ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 ∧ X ∈ ℂ ∖ 0 ∧ x ∈ ℂ ∖ 0 1 ∧ y ∈ ℂ ∖ 0 → log ⁡ y log ⁡ x ∈ V
3 2 ralrimivva ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 ∧ X ∈ ℂ ∖ 0 → ∀ x ∈ ℂ ∖ 0 1 ∀ y ∈ ℂ ∖ 0 log ⁡ y log ⁡ x ∈ V
4 cnex ⊢ ℂ ∈ V
5 difexg ⊢ ℂ ∈ V → ℂ ∖ 0 ∈ V
6 4 5 mp1i ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 ∧ X ∈ ℂ ∖ 0 → ℂ ∖ 0 ∈ V
7 eldifpr ⊢ B ∈ ℂ ∖ 0 1 ↔ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1
8 7 biranri ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 ∧ X ∈ ℂ ∖ 0 → B ∈ ℂ ∖ 0 1
9 simpr ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 ∧ X ∈ ℂ ∖ 0 → X ∈ ℂ ∖ 0
10 1 3 6 8 9 fvmpocurryd ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 ∧ X ∈ ℂ ∖ 0 → curry logb ⁡ B ⁡ X = log B X