Definition df-logbALT 42316

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- 42315	. 2 class log_
2		vb	. . 3 setvar 𝑏
3		cc 9813	. . . 4 class ℂ
4		cc0 9815	. . . . 5 class 0
5		c1 9816	. . . . 5 class 1
6	4, 5	cpr 4127	. . . 4 class {0, 1}
7	3, 6	cdif 3537	. . 3 class (ℂ ∖ {0, 1})
8		vx	. . . 4 setvar 𝑥
9	4	csn 4125	. . . . 5 class {0}
10	3, 9	cdif 3537	. . . 4 class (ℂ ∖ {0})
11	8	cv 1474	. . . . . 6 class 𝑥
12		clog 24105	. . . . . 6 class log
13	11, 12	cfv 5804	. . . . 5 class (log‘𝑥)
14	2	cv 1474	. . . . . 6 class 𝑏
15	14, 12	cfv 5804	. . . . 5 class (log‘𝑏)
16		cdiv 10563	. . . . 5 class /
17	13, 15, 16	co 6549	. . . 4 class ((log‘𝑥) / (log‘𝑏))
18	8, 10, 17	cmpt 4643	. . 3 class (𝑥 ∈ (ℂ ∖ {0}) ↦ ((log‘𝑥) / (log‘𝑏)))
19	2, 7, 18	cmpt 4643	. 2 class (𝑏 ∈ (ℂ ∖ {0, 1}) ↦ (𝑥 ∈ (ℂ ∖ {0}) ↦ ((log‘𝑥) / (log‘𝑏))))
20	1, 19	wceq 1475	1 wff log_ = (𝑏 ∈ (ℂ ∖ {0, 1}) ↦ (𝑥 ∈ (ℂ ∖ {0}) ↦ ((log‘𝑥) / (log‘𝑏))))

This definition is referenced by: (None)