Definition df-logbALT 49340

Description: Define the log_ operator. This is the logarithm generalized to an arbitrary base. It can be used as ((log_‘𝐵)‘𝑋) for "log base B of X". This formulation suggested by Mario Carneiro. (Contributed by David A. Wheeler, 14-Jul-2017.) (New usage is discouraged.)

Assertion

Ref	Expression
df-logbALT	⊢ log_ = (𝑏 ∈ (ℂ ∖ {0, 1}) ↦ (𝑥 ∈ (ℂ ∖ {0}) ↦ ((log‘𝑥) / (log‘𝑏))))

Distinct variable group:   𝑥,𝑏

Detailed syntax breakdown of Definition df-logbALT

Step	Hyp	Ref	Expression
1		clog- 49339	. 2 class log_
2		vb	. . 3 setvar 𝑏
3		cc 11154	. . . 4 class ℂ
4		cc0 11156	. . . . 5 class 0
5		c1 11157	. . . . 5 class 1
6	4, 5	cpr 4627	. . . 4 class {0, 1}
7	3, 6	cdif 3947	. . 3 class (ℂ ∖ {0, 1})
8		vx	. . . 4 setvar 𝑥
9	4	csn 4625	. . . . 5 class {0}
10	3, 9	cdif 3947	. . . 4 class (ℂ ∖ {0})
11	8	cv 1538	. . . . . 6 class 𝑥
12		clog 26597	. . . . . 6 class log
13	11, 12	cfv 6560	. . . . 5 class (log‘𝑥)
14	2	cv 1538	. . . . . 6 class 𝑏
15	14, 12	cfv 6560	. . . . 5 class (log‘𝑏)
16		cdiv 11921	. . . . 5 class /
17	13, 15, 16	co 7432	. . . 4 class ((log‘𝑥) / (log‘𝑏))
18	8, 10, 17	cmpt 5224	. . 3 class (𝑥 ∈ (ℂ ∖ {0}) ↦ ((log‘𝑥) / (log‘𝑏)))
19	2, 7, 18	cmpt 5224	. 2 class (𝑏 ∈ (ℂ ∖ {0, 1}) ↦ (𝑥 ∈ (ℂ ∖ {0}) ↦ ((log‘𝑥) / (log‘𝑏))))
20	1, 19	wceq 1539	1 wff log_ = (𝑏 ∈ (ℂ ∖ {0, 1}) ↦ (𝑥 ∈ (ℂ ∖ {0}) ↦ ((log‘𝑥) / (log‘𝑏))))

This definition is referenced by: (None)