Theorem logbmpt 24820

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

Assertion

Ref	Expression
logbmpt	⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → (curry logb ‘𝐵) = (𝑦 ∈ (ℂ ∖ {0}) ↦ ((log‘𝑦) / (log‘𝐵))))

Distinct variable group:   𝑦,𝐵

Proof of Theorem logbmpt

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-logb 24797	. . 3 ⊢ logb = (𝑥 ∈ (ℂ ∖ {0, 1}), 𝑦 ∈ (ℂ ∖ {0}) ↦ ((log‘𝑦) / (log‘𝑥)))
2		ovexd 6878	. . . 4 ⊢ (((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) ∧ (𝑥 ∈ (ℂ ∖ {0, 1}) ∧ 𝑦 ∈ (ℂ ∖ {0}))) → ((log‘𝑦) / (log‘𝑥)) ∈ V)
3	2	ralrimivva 3118	. . 3 ⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → ∀𝑥 ∈ (ℂ ∖ {0, 1})∀𝑦 ∈ (ℂ ∖ {0})((log‘𝑦) / (log‘𝑥)) ∈ V)
4		ax-1cn 10249	. . . . . 6 ⊢ 1 ∈ ℂ
5		ax-1ne0 10260	. . . . . . 7 ⊢ 1 ≠ 0
6		elsng 4350	. . . . . . . 8 ⊢ (1 ∈ ℂ → (1 ∈ {0} ↔ 1 = 0))
7	4, 6	ax-mp 5	. . . . . . 7 ⊢ (1 ∈ {0} ↔ 1 = 0)
8	5, 7	nemtbir 3032	. . . . . 6 ⊢ ¬ 1 ∈ {0}
9		eldif 3744	. . . . . 6 ⊢ (1 ∈ (ℂ ∖ {0}) ↔ (1 ∈ ℂ ∧ ¬ 1 ∈ {0}))
10	4, 8, 9	mpbir2an 702	. . . . 5 ⊢ 1 ∈ (ℂ ∖ {0})
11	10	ne0ii 4090	. . . 4 ⊢ (ℂ ∖ {0}) ≠ ∅
12	11	a1i 11	. . 3 ⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → (ℂ ∖ {0}) ≠ ∅)
13		cnex 10272	. . . . 5 ⊢ ℂ ∈ V
14		difexg 4971	. . . . 5 ⊢ (ℂ ∈ V → (ℂ ∖ {0}) ∈ V)
15	13, 14	ax-mp 5	. . . 4 ⊢ (ℂ ∖ {0}) ∈ V
16	15	a1i 11	. . 3 ⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → (ℂ ∖ {0}) ∈ V)
17		eldifpr 4364	. . . 4 ⊢ (𝐵 ∈ (ℂ ∖ {0, 1}) ↔ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1))
18	17	biimpri 219	. . 3 ⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → 𝐵 ∈ (ℂ ∖ {0, 1}))
19	1, 3, 12, 16, 18	mpt2curryvald 7601	. 2 ⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → (curry logb ‘𝐵) = (𝑦 ∈ (ℂ ∖ {0}) ↦ ⦋𝐵 / 𝑥⦌((log‘𝑦) / (log‘𝑥))))
20		csbov2g 6889	. . . . 5 ⊢ (𝐵 ∈ ℂ → ⦋𝐵 / 𝑥⦌((log‘𝑦) / (log‘𝑥)) = ((log‘𝑦) / ⦋𝐵 / 𝑥⦌(log‘𝑥)))
21		csbfv 6423	. . . . . . 7 ⊢ ⦋𝐵 / 𝑥⦌(log‘𝑥) = (log‘𝐵)
22	21	a1i 11	. . . . . 6 ⊢ (𝐵 ∈ ℂ → ⦋𝐵 / 𝑥⦌(log‘𝑥) = (log‘𝐵))
23	22	oveq2d 6860	. . . . 5 ⊢ (𝐵 ∈ ℂ → ((log‘𝑦) / ⦋𝐵 / 𝑥⦌(log‘𝑥)) = ((log‘𝑦) / (log‘𝐵)))
24	20, 23	eqtrd 2799	. . . 4 ⊢ (𝐵 ∈ ℂ → ⦋𝐵 / 𝑥⦌((log‘𝑦) / (log‘𝑥)) = ((log‘𝑦) / (log‘𝐵)))
25	24	3ad2ant1 1163	. . 3 ⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → ⦋𝐵 / 𝑥⦌((log‘𝑦) / (log‘𝑥)) = ((log‘𝑦) / (log‘𝐵)))
26	25	mpteq2dv 4906	. 2 ⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → (𝑦 ∈ (ℂ ∖ {0}) ↦ ⦋𝐵 / 𝑥⦌((log‘𝑦) / (log‘𝑥))) = (𝑦 ∈ (ℂ ∖ {0}) ↦ ((log‘𝑦) / (log‘𝐵))))
27	19, 26	eqtrd 2799	1 ⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → (curry logb ‘𝐵) = (𝑦 ∈ (ℂ ∖ {0}) ↦ ((log‘𝑦) / (log‘𝐵))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 197   ∧ wa 384   ∧ w3a 1107   = wceq 1652   ∈ wcel 2155   ≠ wne 2937  Vcvv 3350  ⦋csb 3693   ∖ cdif 3731  ∅c0 4081  {csn 4336  {cpr 4338   ↦ cmpt 4890  ‘cfv 6070  (class class class)co 6844  curry ccur 7596  ℂcc 10189  0cc0 10191  1c1 10192   / cdiv 10940  logclog 24595   log_b clogb 24796

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7149  ax-cnex 10247  ax-1cn 10249  ax-1ne0 10260

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-nul 4082  df-if 4246  df-sn 4337  df-pr 4339  df-op 4343  df-uni 4597  df-iun 4680  df-br 4812  df-opab 4874  df-mpt 4891  df-id 5187  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-ov 6847  df-oprab 6848  df-mpt2 6849  df-1st 7368  df-2nd 7369  df-cur 7598  df-logb 24797

This theorem is referenced by:  logbf  24821  relogbf  24823  logblog  24824