Definition df-dig 42188

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 12860. 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 42187	. 2 class digit
2		vb	. . 3 setvar 𝑏
3		cn 10897	. . 3 class ℕ
4		vk	. . . 4 setvar 𝑘
5		vr	. . . 4 setvar 𝑟
6		cz 11254	. . . 4 class ℤ
7		cc0 9815	. . . . 5 class 0
8		cpnf 9950	. . . . 5 class +∞
9		cico 12048	. . . . 5 class [,)
10	7, 8, 9	co 6549	. . . 4 class (0[,)+∞)
11	2	cv 1474	. . . . . . . 8 class 𝑏
12	4	cv 1474	. . . . . . . . 9 class 𝑘
13	12	cneg 10146	. . . . . . . 8 class -𝑘
14		cexp 12722	. . . . . . . 8 class ↑
15	11, 13, 14	co 6549	. . . . . . 7 class (𝑏↑-𝑘)
16	5	cv 1474	. . . . . . 7 class 𝑟
17		cmul 9820	. . . . . . 7 class ·
18	15, 16, 17	co 6549	. . . . . 6 class ((𝑏↑-𝑘) · 𝑟)
19		cfl 12453	. . . . . 6 class ⌊
20	18, 19	cfv 5804	. . . . 5 class (⌊‘((𝑏↑-𝑘) · 𝑟))
21		cmo 12530	. . . . 5 class mod
22	20, 11, 21	co 6549	. . . 4 class ((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏)
23	4, 5, 6, 10, 22	cmpt2 6551	. . 3 class (𝑘 ∈ ℤ, 𝑟 ∈ (0[,)+∞) ↦ ((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏))
24	2, 3, 23	cmpt 4643	. 2 class (𝑏 ∈ ℕ ↦ (𝑘 ∈ ℤ, 𝑟 ∈ (0[,)+∞) ↦ ((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏)))
25	1, 24	wceq 1475	1 wff digit = (𝑏 ∈ ℕ ↦ (𝑘 ∈ ℤ, 𝑟 ∈ (0[,)+∞) ↦ ((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏)))

This definition is referenced by:  digfval  42189