Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-logb GIF version

Definition df-logb 13208
 Description: Define the logb operator. This is the logarithm generalized to an arbitrary base. It can be used as (𝐵 logb 𝑋) for "log base B of X". In the most common traditional notation, base B is a subscript of "log". The definition will only be useful where 𝑥 is a positive real apart from one and where 𝑦 is a positive real, so the choice of (ℂ ∖ {0, 1}) and (ℂ ∖ {0}) is somewhat arbitrary (we adopt the definition used in set.mm). (Contributed by David A. Wheeler, 21-Jan-2017.)
Assertion
Ref Expression
df-logb logb = (𝑥 ∈ (ℂ ∖ {0, 1}), 𝑦 ∈ (ℂ ∖ {0}) ↦ ((log‘𝑦) / (log‘𝑥)))
Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-logb
StepHypRef Expression
1 clogb 13207 . 2 class logb
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cc 7709 . . . 4 class
5 cc0 7711 . . . . 5 class 0
6 c1 7712 . . . . 5 class 1
75, 6cpr 3557 . . . 4 class {0, 1}
84, 7cdif 3095 . . 3 class (ℂ ∖ {0, 1})
95csn 3556 . . . 4 class {0}
104, 9cdif 3095 . . 3 class (ℂ ∖ {0})
113cv 1331 . . . . 5 class 𝑦
12 clog 13124 . . . . 5 class log
1311, 12cfv 5163 . . . 4 class (log‘𝑦)
142cv 1331 . . . . 5 class 𝑥
1514, 12cfv 5163 . . . 4 class (log‘𝑥)
16 cdiv 8524 . . . 4 class /
1713, 15, 16co 5814 . . 3 class ((log‘𝑦) / (log‘𝑥))
182, 3, 8, 10, 17cmpo 5816 . 2 class (𝑥 ∈ (ℂ ∖ {0, 1}), 𝑦 ∈ (ℂ ∖ {0}) ↦ ((log‘𝑦) / (log‘𝑥)))
191, 18wceq 1332 1 wff logb = (𝑥 ∈ (ℂ ∖ {0, 1}), 𝑦 ∈ (ℂ ∖ {0}) ↦ ((log‘𝑦) / (log‘𝑥)))
 Colors of variables: wff set class This definition is referenced by:  rplogbval  13209
 Copyright terms: Public domain W3C validator