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 45676
 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- 45675 . 2 class log_
2 vb . . 3 setvar 𝑏
3 cc 10566 . . . 4 class
4 cc0 10568 . . . . 5 class 0
5 c1 10569 . . . . 5 class 1
64, 5cpr 4525 . . . 4 class {0, 1}
73, 6cdif 3856 . . 3 class (ℂ ∖ {0, 1})
8 vx . . . 4 setvar 𝑥
94csn 4523 . . . . 5 class {0}
103, 9cdif 3856 . . . 4 class (ℂ ∖ {0})
118cv 1538 . . . . . 6 class 𝑥
12 clog 25238 . . . . . 6 class log
1311, 12cfv 6336 . . . . 5 class (log‘𝑥)
142cv 1538 . . . . . 6 class 𝑏
1514, 12cfv 6336 . . . . 5 class (log‘𝑏)
16 cdiv 11328 . . . . 5 class /
1713, 15, 16co 7151 . . . 4 class ((log‘𝑥) / (log‘𝑏))
188, 10, 17cmpt 5113 . . 3 class (𝑥 ∈ (ℂ ∖ {0}) ↦ ((log‘𝑥) / (log‘𝑏)))
192, 7, 18cmpt 5113 . 2 class (𝑏 ∈ (ℂ ∖ {0, 1}) ↦ (𝑥 ∈ (ℂ ∖ {0}) ↦ ((log‘𝑥) / (log‘𝑏))))
201, 19wceq 1539 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