Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-dig Structured version   Visualization version   GIF version

Definition df-dig 44584
Description: Definition of an operation to obtain the 𝑘 th digit of a nonnegative real number 𝑟 in the positional system with base 𝑏. 𝑘 = − 1 corresponds to the first digit of the fractional part (for 𝑏 = 10 the first digit after the decimal point), 𝑘 = 0 corresponds to the last digit of the integer part (for 𝑏 = 10 the first digit before the decimal point). See also digit1 13586. Examples (not formal): ( 234.567 ( digit ` 10 ) 0 ) = 4; ( 2.567 ( digit ` 10 ) -2 ) = 6; ( 2345.67 ( digit ` 10 ) 2 ) = 3. (Contributed by AV, 16-May-2020.)
Assertion
Ref Expression
df-dig digit = (𝑏 ∈ ℕ ↦ (𝑘 ∈ ℤ, 𝑟 ∈ (0[,)+∞) ↦ ((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏)))
Distinct variable group:   𝑘,𝑏,𝑟

Detailed syntax breakdown of Definition df-dig
StepHypRef Expression
1 cdig 44583 . 2 class digit
2 vb . . 3 setvar 𝑏
3 cn 11626 . . 3 class
4 vk . . . 4 setvar 𝑘
5 vr . . . 4 setvar 𝑟
6 cz 11969 . . . 4 class
7 cc0 10525 . . . . 5 class 0
8 cpnf 10660 . . . . 5 class +∞
9 cico 12728 . . . . 5 class [,)
107, 8, 9co 7145 . . . 4 class (0[,)+∞)
112cv 1527 . . . . . . . 8 class 𝑏
124cv 1527 . . . . . . . . 9 class 𝑘
1312cneg 10859 . . . . . . . 8 class -𝑘
14 cexp 13417 . . . . . . . 8 class
1511, 13, 14co 7145 . . . . . . 7 class (𝑏↑-𝑘)
165cv 1527 . . . . . . 7 class 𝑟
17 cmul 10530 . . . . . . 7 class ·
1815, 16, 17co 7145 . . . . . 6 class ((𝑏↑-𝑘) · 𝑟)
19 cfl 13148 . . . . . 6 class
2018, 19cfv 6348 . . . . 5 class (⌊‘((𝑏↑-𝑘) · 𝑟))
21 cmo 13225 . . . . 5 class mod
2220, 11, 21co 7145 . . . 4 class ((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏)
234, 5, 6, 10, 22cmpo 7147 . . 3 class (𝑘 ∈ ℤ, 𝑟 ∈ (0[,)+∞) ↦ ((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏))
242, 3, 23cmpt 5137 . 2 class (𝑏 ∈ ℕ ↦ (𝑘 ∈ ℤ, 𝑟 ∈ (0[,)+∞) ↦ ((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏)))
251, 24wceq 1528 1 wff digit = (𝑏 ∈ ℕ ↦ (𝑘 ∈ ℤ, 𝑟 ∈ (0[,)+∞) ↦ ((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏)))
Colors of variables: wff setvar class
This definition is referenced by:  digfval  44585
  Copyright terms: Public domain W3C validator