Definition df-logbALT 44872

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- 44871	. 2 class log_
2		vb	. . 3 setvar 𝑏
3		cc 10538	. . . 4 class ℂ
4		cc0 10540	. . . . 5 class 0
5		c1 10541	. . . . 5 class 1
6	4, 5	cpr 4572	. . . 4 class {0, 1}
7	3, 6	cdif 3936	. . 3 class (ℂ ∖ {0, 1})
8		vx	. . . 4 setvar 𝑥
9	4	csn 4570	. . . . 5 class {0}
10	3, 9	cdif 3936	. . . 4 class (ℂ ∖ {0})
11	8	cv 1535	. . . . . 6 class 𝑥
12		clog 25141	. . . . . 6 class log
13	11, 12	cfv 6358	. . . . 5 class (log‘𝑥)
14	2	cv 1535	. . . . . 6 class 𝑏
15	14, 12	cfv 6358	. . . . 5 class (log‘𝑏)
16		cdiv 11300	. . . . 5 class /
17	13, 15, 16	co 7159	. . . 4 class ((log‘𝑥) / (log‘𝑏))
18	8, 10, 17	cmpt 5149	. . 3 class (𝑥 ∈ (ℂ ∖ {0}) ↦ ((log‘𝑥) / (log‘𝑏)))
19	2, 7, 18	cmpt 5149	. 2 class (𝑏 ∈ (ℂ ∖ {0, 1}) ↦ (𝑥 ∈ (ℂ ∖ {0}) ↦ ((log‘𝑥) / (log‘𝑏))))
20	1, 19	wceq 1536	1 wff log_ = (𝑏 ∈ (ℂ ∖ {0, 1}) ↦ (𝑥 ∈ (ℂ ∖ {0}) ↦ ((log‘𝑥) / (log‘𝑏))))

This definition is referenced by: (None)