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 ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( curry logb ‘ 𝐵 ) = ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ( log ‘ 𝑦 ) / ( log ‘ 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 df-logb ⊢ logb = ( 𝑥 ∈ ( ℂ ∖ { 0 , 1 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ( log ‘ 𝑦 ) / ( log ‘ 𝑥 ) ) )
2 ovexd ⊢ ( ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) ∧ ( 𝑥 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ) → ( ( log ‘ 𝑦 ) / ( log ‘ 𝑥 ) ) ∈ V )
3 2 ralrimivva ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ∀ 𝑥 ∈ ( ℂ ∖ { 0 , 1 } ) ∀ 𝑦 ∈ ( ℂ ∖ { 0 } ) ( ( log ‘ 𝑦 ) / ( log ‘ 𝑥 ) ) ∈ 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 ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( ℂ ∖ { 0 } ) ≠ ∅ )
13 cnex ⊢ ℂ ∈ V
14 13 difexi ⊢ ( ℂ ∖ { 0 } ) ∈ V
15 14 a1i ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( ℂ ∖ { 0 } ) ∈ V )
16 eldifpr ⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ↔ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
17 16 biimpri ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) )
18 1 3 12 15 17 mpocurryvald ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( curry logb ‘ 𝐵 ) = ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ⦋ 𝐵 / 𝑥 ⦌ ( ( log ‘ 𝑦 ) / ( log ‘ 𝑥 ) ) ) )
19 csbov2g ⊢ ( 𝐵 ∈ ℂ → ⦋ 𝐵 / 𝑥 ⦌ ( ( log ‘ 𝑦 ) / ( log ‘ 𝑥 ) ) = ( ( log ‘ 𝑦 ) / ⦋ 𝐵 / 𝑥 ⦌ ( log ‘ 𝑥 ) ) )
20 csbfv ⊢ ⦋ 𝐵 / 𝑥 ⦌ ( log ‘ 𝑥 ) = ( log ‘ 𝐵 )
21 20 a1i ⊢ ( 𝐵 ∈ ℂ → ⦋ 𝐵 / 𝑥 ⦌ ( log ‘ 𝑥 ) = ( log ‘ 𝐵 ) )
22 21 oveq2d ⊢ ( 𝐵 ∈ ℂ → ( ( log ‘ 𝑦 ) / ⦋ 𝐵 / 𝑥 ⦌ ( log ‘ 𝑥 ) ) = ( ( log ‘ 𝑦 ) / ( log ‘ 𝐵 ) ) )
23 19 22 eqtrd ⊢ ( 𝐵 ∈ ℂ → ⦋ 𝐵 / 𝑥 ⦌ ( ( log ‘ 𝑦 ) / ( log ‘ 𝑥 ) ) = ( ( log ‘ 𝑦 ) / ( log ‘ 𝐵 ) ) )
24 23 3ad2ant1 ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ⦋ 𝐵 / 𝑥 ⦌ ( ( log ‘ 𝑦 ) / ( log ‘ 𝑥 ) ) = ( ( log ‘ 𝑦 ) / ( log ‘ 𝐵 ) ) )
25 24 mpteq2dv ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ⦋ 𝐵 / 𝑥 ⦌ ( ( log ‘ 𝑦 ) / ( log ‘ 𝑥 ) ) ) = ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ( log ‘ 𝑦 ) / ( log ‘ 𝐵 ) ) ) )
26 18 25 eqtrd ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( curry logb ‘ 𝐵 ) = ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ( log ‘ 𝑦 ) / ( log ‘ 𝐵 ) ) ) )