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 ⊢ 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 biimpri ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 → B ∈ ℂ ∖ 0 1
9 8 adantr ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 ∧ X ∈ ℂ ∖ 0 → B ∈ ℂ ∖ 0 1
10 simpr ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 ∧ X ∈ ℂ ∖ 0 → X ∈ ℂ ∖ 0
11 1 3 6 9 10 fvmpocurryd ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 ∧ X ∈ ℂ ∖ 0 → curry logb ⁡ B ⁡ X = log B X