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→currylogb⁡B=y∈ℂ∖0⟼log⁡ylog⁡B

Proof

Step Hyp Ref Expression
1 df-logb ⊢logb=x∈ℂ∖01,y∈ℂ∖0⟼log⁡ylog⁡x
2 ovexd ⊢B∈ℂ∧B≠0∧B≠1∧x∈ℂ∖01∧y∈ℂ∖0→log⁡ylog⁡x∈V
3 2 ralrimivva ⊢B∈ℂ∧B≠0∧B≠1→∀x∈ℂ∖01∀y∈ℂ∖0log⁡ylog⁡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∈ℂ∖01↔B∈ℂ∧B≠0∧B≠1
17 16 biimpri ⊢B∈ℂ∧B≠0∧B≠1→B∈ℂ∖01
18 1 3 12 15 17 mpocurryvald ⊢B∈ℂ∧B≠0∧B≠1→currylogb⁡B=y∈ℂ∖0⟼⦋B/x⦌log⁡ylog⁡x
19 csbov2g ⊢B∈ℂ→⦋B/x⦌log⁡ylog⁡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⁡ylog⁡B
23 19 22 eqtrd ⊢B∈ℂ→⦋B/x⦌log⁡ylog⁡x=log⁡ylog⁡B
24 23 3ad2ant1 ⊢B∈ℂ∧B≠0∧B≠1→⦋B/x⦌log⁡ylog⁡x=log⁡ylog⁡B
25 24 mpteq2dv ⊢B∈ℂ∧B≠0∧B≠1→y∈ℂ∖0⟼⦋B/x⦌log⁡ylog⁡x=y∈ℂ∖0⟼log⁡ylog⁡B
26 18 25 eqtrd ⊢B∈ℂ∧B≠0∧B≠1→currylogb⁡B=y∈ℂ∖0⟼log⁡ylog⁡B