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 44801
 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 13583. 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 44800 . 2 class digit
2 vb . . 3 setvar 𝑏
3 cn 11616 . . 3 class
4 vk . . . 4 setvar 𝑘
5 vr . . . 4 setvar 𝑟
6 cz 11960 . . . 4 class
7 cc0 10515 . . . . 5 class 0
8 cpnf 10650 . . . . 5 class +∞
9 cico 12719 . . . . 5 class [,)
107, 8, 9co 7133 . . . 4 class (0[,)+∞)
112cv 1536 . . . . . . . 8 class 𝑏
124cv 1536 . . . . . . . . 9 class 𝑘
1312cneg 10849 . . . . . . . 8 class -𝑘
14 cexp 13414 . . . . . . . 8 class
1511, 13, 14co 7133 . . . . . . 7 class (𝑏↑-𝑘)
165cv 1536 . . . . . . 7 class 𝑟
17 cmul 10520 . . . . . . 7 class ·
1815, 16, 17co 7133 . . . . . 6 class ((𝑏↑-𝑘) · 𝑟)
19 cfl 13144 . . . . . 6 class
2018, 19cfv 6331 . . . . 5 class (⌊‘((𝑏↑-𝑘) · 𝑟))
21 cmo 13221 . . . . 5 class mod
2220, 11, 21co 7133 . . . 4 class ((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏)
234, 5, 6, 10, 22cmpo 7135 . . 3 class (𝑘 ∈ ℤ, 𝑟 ∈ (0[,)+∞) ↦ ((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏))
242, 3, 23cmpt 5122 . 2 class (𝑏 ∈ ℕ ↦ (𝑘 ∈ ℤ, 𝑟 ∈ (0[,)+∞) ↦ ((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏)))
251, 24wceq 1537 1 wff digit = (𝑏 ∈ ℕ ↦ (𝑘 ∈ ℤ, 𝑟 ∈ (0[,)+∞) ↦ ((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏)))
 Colors of variables: wff setvar class This definition is referenced by:  digfval  44802
 Copyright terms: Public domain W3C validator