Users' Mathboxes Mathbox for David A. Wheeler < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-logbALT Structured version   Visualization version   GIF version

Definition df-logbALT 42272
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
StepHypRef Expression
1 clog- 42271 . 2 class log_
2 vb . . 3 setvar 𝑏
3 cc 9790 . . . 4 class
4 cc0 9792 . . . . 5 class 0
5 c1 9793 . . . . 5 class 1
64, 5cpr 4126 . . . 4 class {0, 1}
73, 6cdif 3536 . . 3 class (ℂ ∖ {0, 1})
8 vx . . . 4 setvar 𝑥
94csn 4124 . . . . 5 class {0}
103, 9cdif 3536 . . . 4 class (ℂ ∖ {0})
118cv 1473 . . . . . 6 class 𝑥
12 clog 24022 . . . . . 6 class log
1311, 12cfv 5790 . . . . 5 class (log‘𝑥)
142cv 1473 . . . . . 6 class 𝑏
1514, 12cfv 5790 . . . . 5 class (log‘𝑏)
16 cdiv 10533 . . . . 5 class /
1713, 15, 16co 6527 . . . 4 class ((log‘𝑥) / (log‘𝑏))
188, 10, 17cmpt 4637 . . 3 class (𝑥 ∈ (ℂ ∖ {0}) ↦ ((log‘𝑥) / (log‘𝑏)))
192, 7, 18cmpt 4637 . 2 class (𝑏 ∈ (ℂ ∖ {0, 1}) ↦ (𝑥 ∈ (ℂ ∖ {0}) ↦ ((log‘𝑥) / (log‘𝑏))))
201, 19wceq 1474 1 wff log_ = (𝑏 ∈ (ℂ ∖ {0, 1}) ↦ (𝑥 ∈ (ℂ ∖ {0}) ↦ ((log‘𝑥) / (log‘𝑏))))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator