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 42161
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 12993. 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 42160 . 2 class digit
2 vb . . 3 setvar 𝑏
3 cn 11017 . . 3 class
4 vk . . . 4 setvar 𝑘
5 vr . . . 4 setvar 𝑟
6 cz 11374 . . . 4 class
7 cc0 9933 . . . . 5 class 0
8 cpnf 10068 . . . . 5 class +∞
9 cico 12174 . . . . 5 class [,)
107, 8, 9co 6647 . . . 4 class (0[,)+∞)
112cv 1481 . . . . . . . 8 class 𝑏
124cv 1481 . . . . . . . . 9 class 𝑘
1312cneg 10264 . . . . . . . 8 class -𝑘
14 cexp 12855 . . . . . . . 8 class
1511, 13, 14co 6647 . . . . . . 7 class (𝑏↑-𝑘)
165cv 1481 . . . . . . 7 class 𝑟
17 cmul 9938 . . . . . . 7 class ·
1815, 16, 17co 6647 . . . . . 6 class ((𝑏↑-𝑘) · 𝑟)
19 cfl 12586 . . . . . 6 class
2018, 19cfv 5886 . . . . 5 class (⌊‘((𝑏↑-𝑘) · 𝑟))
21 cmo 12663 . . . . 5 class mod
2220, 11, 21co 6647 . . . 4 class ((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏)
234, 5, 6, 10, 22cmpt2 6649 . . 3 class (𝑘 ∈ ℤ, 𝑟 ∈ (0[,)+∞) ↦ ((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏))
242, 3, 23cmpt 4727 . 2 class (𝑏 ∈ ℕ ↦ (𝑘 ∈ ℤ, 𝑟 ∈ (0[,)+∞) ↦ ((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏)))
251, 24wceq 1482 1 wff digit = (𝑏 ∈ ℕ ↦ (𝑘 ∈ ℤ, 𝑟 ∈ (0[,)+∞) ↦ ((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏)))
Colors of variables: wff setvar class
This definition is referenced by:  digfval  42162
  Copyright terms: Public domain W3C validator