Definition df-dig

Description: Definition of an operation to obtain the k th digit of a nonnegative real number r in the positional system with base b . k = - 1 corresponds to the first digit of the fractional part (for b = 10 the first digit after the decimal point), k = 0 corresponds to the last digit of the integer part (for b = 10 the first digit before the decimal point). See also digit1 . Examples (not formal): ( 234.567 ( digit `10 ) 0 ) = 4; ( 2.567 ( digit10 ) -2 ) = 6; ( 2345.67 ( digit` 10 ) 2 ) = 3. (Contributed by AV, 16-May-2020)

	Ref	Expression
Assertion	df-dig	⊢ digit = ( 𝑏 ∈ ℕ ↦ ( 𝑘 ∈ ℤ , 𝑟 ∈ ( 0 [,) +∞ ) ↦ ( ( ⌊ ‘ ( ( 𝑏 ↑ - 𝑘 ) · 𝑟 ) ) mod 𝑏 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdig	⊢ digit
1		vb	⊢ 𝑏
2		cn	⊢ ℕ
3		vk	⊢ 𝑘
4		cz	⊢ ℤ
5		vr	⊢ 𝑟
6		cc0	⊢ 0
7		cico	⊢ [,)
8		cpnf	⊢ +∞
9	6 8 7	co	⊢ ( 0 [,) +∞ )
10		cfl	⊢ ⌊
11	1	cv	⊢ 𝑏
12		cexp	⊢ ↑
13	3	cv	⊢ 𝑘
14	13	cneg	⊢ - 𝑘
15	11 14 12	co	⊢ ( 𝑏 ↑ - 𝑘 )
16		cmul	⊢ ·
17	5	cv	⊢ 𝑟
18	15 17 16	co	⊢ ( ( 𝑏 ↑ - 𝑘 ) · 𝑟 )
19	18 10	cfv	⊢ ( ⌊ ‘ ( ( 𝑏 ↑ - 𝑘 ) · 𝑟 ) )
20		cmo	⊢ mod
21	19 11 20	co	⊢ ( ( ⌊ ‘ ( ( 𝑏 ↑ - 𝑘 ) · 𝑟 ) ) mod 𝑏 )
22	3 5 4 9 21	cmpo	⊢ ( 𝑘 ∈ ℤ , 𝑟 ∈ ( 0 [,) +∞ ) ↦ ( ( ⌊ ‘ ( ( 𝑏 ↑ - 𝑘 ) · 𝑟 ) ) mod 𝑏 ) )
23	1 2 22	cmpt	⊢ ( 𝑏 ∈ ℕ ↦ ( 𝑘 ∈ ℤ , 𝑟 ∈ ( 0 [,) +∞ ) ↦ ( ( ⌊ ‘ ( ( 𝑏 ↑ - 𝑘 ) · 𝑟 ) ) mod 𝑏 ) ) )
24	0 23	wceq	⊢ digit = ( 𝑏 ∈ ℕ ↦ ( 𝑘 ∈ ℤ , 𝑟 ∈ ( 0 [,) +∞ ) ↦ ( ( ⌊ ‘ ( ( 𝑏 ↑ - 𝑘 ) · 𝑟 ) ) mod 𝑏 ) ) )