Definition df-dig 48517

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 14276. 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

Step	Hyp	Ref	Expression
1		cdig 48516	. 2 class digit
2		vb	. . 3 setvar 𝑏
3		cn 12266	. . 3 class ℕ
4		vk	. . . 4 setvar 𝑘
5		vr	. . . 4 setvar 𝑟
6		cz 12613	. . . 4 class ℤ
7		cc0 11155	. . . . 5 class 0
8		cpnf 11292	. . . . 5 class +∞
9		cico 13389	. . . . 5 class [,)
10	7, 8, 9	co 7431	. . . 4 class (0[,)+∞)
11	2	cv 1539	. . . . . . . 8 class 𝑏
12	4	cv 1539	. . . . . . . . 9 class 𝑘
13	12	cneg 11493	. . . . . . . 8 class -𝑘
14		cexp 14102	. . . . . . . 8 class ↑
15	11, 13, 14	co 7431	. . . . . . 7 class (𝑏↑-𝑘)
16	5	cv 1539	. . . . . . 7 class 𝑟
17		cmul 11160	. . . . . . 7 class ·
18	15, 16, 17	co 7431	. . . . . 6 class ((𝑏↑-𝑘) · 𝑟)
19		cfl 13830	. . . . . 6 class ⌊
20	18, 19	cfv 6561	. . . . 5 class (⌊‘((𝑏↑-𝑘) · 𝑟))
21		cmo 13909	. . . . 5 class mod
22	20, 11, 21	co 7431	. . . 4 class ((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏)
23	4, 5, 6, 10, 22	cmpo 7433	. . 3 class (𝑘 ∈ ℤ, 𝑟 ∈ (0[,)+∞) ↦ ((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏))
24	2, 3, 23	cmpt 5225	. 2 class (𝑏 ∈ ℕ ↦ (𝑘 ∈ ℤ, 𝑟 ∈ (0[,)+∞) ↦ ((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏)))
25	1, 24	wceq 1540	1 wff digit = (𝑏 ∈ ℕ ↦ (𝑘 ∈ ℤ, 𝑟 ∈ (0[,)+∞) ↦ ((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏)))

This definition is referenced by:  digfval  48518