Metamath Proof Explorer

Theorem logbmpt

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

Ref Expression
Assertion logbmpt ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 → curry logb ⁡ B = y ∈ ℂ ∖ 0 ⟼ log ⁡ y log ⁡ B

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 1 ∧ y ∈ ℂ ∖ 0 → log ⁡ y log ⁡ x ∈ V
3 2 ralrimivva ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 → ∀ x ∈ ℂ ∖ 0 1 ∀ y ∈ ℂ ∖ 0 log ⁡ y log ⁡ x ∈ V
4 ax-1cn ⊢ 1 ∈ ℂ
5 ax-1ne0 ⊢ 1 ≠ 0
6 elsng ⊢ 1 ∈ ℂ → 1 ∈ 0 ↔ 1 = 0
7 4 6 ax-mp ⊢ 1 ∈ 0 ↔ 1 = 0
8 5 7 nemtbir ⊢ ¬ 1 ∈ 0
9 eldif ⊢ 1 ∈ ℂ ∖ 0 ↔ 1 ∈ ℂ ∧ ¬ 1 ∈ 0
10 4 8 9 mpbir2an ⊢ 1 ∈ ℂ ∖ 0
11 10 ne0ii ⊢ ℂ ∖ 0 ≠ ∅
12 11 a1i ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 → ℂ ∖ 0 ≠ ∅
13 cnex ⊢ ℂ ∈ V
14 13 difexi ⊢ ℂ ∖ 0 ∈ V
15 14 a1i ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 → ℂ ∖ 0 ∈ V
16 eldifpr ⊢ B ∈ ℂ ∖ 0 1 ↔ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1
17 16 biimpri ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 → B ∈ ℂ ∖ 0 1
18 1 3 12 15 17 mpocurryvald ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 → curry logb ⁡ B = y ∈ ℂ ∖ 0 ⟼ ⦋ B / x⦌ log ⁡ y log ⁡ x
19 csbov2g ⊢ B ∈ ℂ → ⦋ B / x⦌ log ⁡ y log ⁡ x = log ⁡ y ⦋ B / x⦌ log ⁡ x
20 csbfv ⊢ ⦋ B / x⦌ log ⁡ x = log ⁡ B
21 20 a1i ⊢ B ∈ ℂ → ⦋ B / x⦌ log ⁡ x = log ⁡ B
22 21 oveq2d ⊢ B ∈ ℂ → log ⁡ y ⦋ B / x⦌ log ⁡ x = log ⁡ y log ⁡ B
23 19 22 eqtrd ⊢ B ∈ ℂ → ⦋ B / x⦌ log ⁡ y log ⁡ x = log ⁡ y log ⁡ B
24 23 3ad2ant1 ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 → ⦋ B / x⦌ log ⁡ y log ⁡ x = log ⁡ y log ⁡ B
25 24 mpteq2dv ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 → y ∈ ℂ ∖ 0 ⟼ ⦋ B / x⦌ log ⁡ y log ⁡ x = y ∈ ℂ ∖ 0 ⟼ log ⁡ y log ⁡ B
26 18 25 eqtrd ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 → curry logb ⁡ B = y ∈ ℂ ∖ 0 ⟼ log ⁡ y log ⁡ B