Definition df-dig 42390

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 12998. 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 = ( b e. NN |-> ( k e. ZZ , r e. ( 0 [,) +oo ) |-> ( ( |_ ` ( ( b ^ -u k ) x. r ) ) mod b ) ) )

Distinct variable group:   k, b, r

Detailed syntax breakdown of Definition df-dig

Step	Hyp	Ref	Expression
1		cdig 42389	. 2 class digit
2		vb	. . 3 setvar b
3		cn 11020	. . 3 class NN
4		vk	. . . 4 setvar k
5		vr	. . . 4 setvar r
6		cz 11377	. . . 4 class ZZ
7		cc0 9936	. . . . 5 class 0
8		cpnf 10071	. . . . 5 class +oo
9		cico 12177	. . . . 5 class [,)
10	7, 8, 9	co 6650	. . . 4 class ( 0 [,) +oo )
11	2	cv 1482	. . . . . . . 8 class b
12	4	cv 1482	. . . . . . . . 9 class k
13	12	cneg 10267	. . . . . . . 8 class -u k
14		cexp 12860	. . . . . . . 8 class ^
15	11, 13, 14	co 6650	. . . . . . 7 class ( b ^ -u k )
16	5	cv 1482	. . . . . . 7 class r
17		cmul 9941	. . . . . . 7 class x.
18	15, 16, 17	co 6650	. . . . . 6 class ( ( b ^ -u k ) x. r )
19		cfl 12591	. . . . . 6 class |_
20	18, 19	cfv 5888	. . . . 5 class ( |_ ` ( ( b ^ -u k ) x. r ) )
21		cmo 12668	. . . . 5 class mod
22	20, 11, 21	co 6650	. . . 4 class ( ( |_ ` ( ( b ^ -u k ) x. r ) ) mod b )
23	4, 5, 6, 10, 22	cmpt2 6652	. . 3 class ( k e. ZZ , r e. ( 0 [,) +oo ) |-> ( ( |_ ` ( ( b ^ -u k ) x. r ) ) mod b ) )
24	2, 3, 23	cmpt 4729	. 2 class ( b e. NN |-> ( k e. ZZ , r e. ( 0 [,) +oo ) |-> ( ( |_ ` ( ( b ^ -u k ) x. r ) ) mod b ) ) )
25	1, 24	wceq 1483	1 wff digit = ( b e. NN |-> ( k e. ZZ , r e. ( 0 [,) +oo ) |-> ( ( |_ ` ( ( b ^ -u k ) x. r ) ) mod b ) ) )

This definition is referenced by:  digfval  42391