Definition df-dig 47330

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 14200. 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 47329	. 2 class digit
2		vb	. . 3 setvar 𝑏
3		cn 12212	. . 3 class ℕ
4		vk	. . . 4 setvar 𝑘
5		vr	. . . 4 setvar 𝑟
6		cz 12558	. . . 4 class ℤ
7		cc0 11110	. . . . 5 class 0
8		cpnf 11245	. . . . 5 class +∞
9		cico 13326	. . . . 5 class [,)
10	7, 8, 9	co 7409	. . . 4 class (0[,)+∞)
11	2	cv 1541	. . . . . . . 8 class 𝑏
12	4	cv 1541	. . . . . . . . 9 class 𝑘
13	12	cneg 11445	. . . . . . . 8 class -𝑘
14		cexp 14027	. . . . . . . 8 class ↑
15	11, 13, 14	co 7409	. . . . . . 7 class (𝑏↑-𝑘)
16	5	cv 1541	. . . . . . 7 class 𝑟
17		cmul 11115	. . . . . . 7 class ·
18	15, 16, 17	co 7409	. . . . . 6 class ((𝑏↑-𝑘) · 𝑟)
19		cfl 13755	. . . . . 6 class ⌊
20	18, 19	cfv 6544	. . . . 5 class (⌊‘((𝑏↑-𝑘) · 𝑟))
21		cmo 13834	. . . . 5 class mod
22	20, 11, 21	co 7409	. . . 4 class ((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏)
23	4, 5, 6, 10, 22	cmpo 7411	. . 3 class (𝑘 ∈ ℤ, 𝑟 ∈ (0[,)+∞) ↦ ((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏))
24	2, 3, 23	cmpt 5232	. 2 class (𝑏 ∈ ℕ ↦ (𝑘 ∈ ℤ, 𝑟 ∈ (0[,)+∞) ↦ ((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏)))
25	1, 24	wceq 1542	1 wff digit = (𝑏 ∈ ℕ ↦ (𝑘 ∈ ℤ, 𝑟 ∈ (0[,)+∞) ↦ ((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏)))

This definition is referenced by:  digfval  47331