Definition df-dig 45830

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 13880. 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 45829	. 2 class digit
2		vb	. . 3 setvar 𝑏
3		cn 11903	. . 3 class ℕ
4		vk	. . . 4 setvar 𝑘
5		vr	. . . 4 setvar 𝑟
6		cz 12249	. . . 4 class ℤ
7		cc0 10802	. . . . 5 class 0
8		cpnf 10937	. . . . 5 class +∞
9		cico 13010	. . . . 5 class [,)
10	7, 8, 9	co 7255	. . . 4 class (0[,)+∞)
11	2	cv 1538	. . . . . . . 8 class 𝑏
12	4	cv 1538	. . . . . . . . 9 class 𝑘
13	12	cneg 11136	. . . . . . . 8 class -𝑘
14		cexp 13710	. . . . . . . 8 class ↑
15	11, 13, 14	co 7255	. . . . . . 7 class (𝑏↑-𝑘)
16	5	cv 1538	. . . . . . 7 class 𝑟
17		cmul 10807	. . . . . . 7 class ·
18	15, 16, 17	co 7255	. . . . . 6 class ((𝑏↑-𝑘) · 𝑟)
19		cfl 13438	. . . . . 6 class ⌊
20	18, 19	cfv 6418	. . . . 5 class (⌊‘((𝑏↑-𝑘) · 𝑟))
21		cmo 13517	. . . . 5 class mod
22	20, 11, 21	co 7255	. . . 4 class ((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏)
23	4, 5, 6, 10, 22	cmpo 7257	. . 3 class (𝑘 ∈ ℤ, 𝑟 ∈ (0[,)+∞) ↦ ((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏))
24	2, 3, 23	cmpt 5153	. 2 class (𝑏 ∈ ℕ ↦ (𝑘 ∈ ℤ, 𝑟 ∈ (0[,)+∞) ↦ ((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏)))
25	1, 24	wceq 1539	1 wff digit = (𝑏 ∈ ℕ ↦ (𝑘 ∈ ℤ, 𝑟 ∈ (0[,)+∞) ↦ ((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏)))

This definition is referenced by:  digfval  45831