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 = ( b e. NN |-> ( k e. ZZ , r e. ( 0 [,) +oo ) |-> ( ( |_ ` ( ( b ^ -u k ) x. r ) ) mod b ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cdig | |- digit |
|
| 1 | vb | |- b |
|
| 2 | cn | |- NN |
|
| 3 | vk | |- k |
|
| 4 | cz | |- ZZ |
|
| 5 | vr | |- r |
|
| 6 | cc0 | |- 0 |
|
| 7 | cico | |- [,) |
|
| 8 | cpnf | |- +oo |
|
| 9 | 6 8 7 | co | |- ( 0 [,) +oo ) |
| 10 | cfl | |- |_ |
|
| 11 | 1 | cv | |- b |
| 12 | cexp | |- ^ |
|
| 13 | 3 | cv | |- k |
| 14 | 13 | cneg | |- -u k |
| 15 | 11 14 12 | co | |- ( b ^ -u k ) |
| 16 | cmul | |- x. |
|
| 17 | 5 | cv | |- r |
| 18 | 15 17 16 | co | |- ( ( b ^ -u k ) x. r ) |
| 19 | 18 10 | cfv | |- ( |_ ` ( ( b ^ -u k ) x. r ) ) |
| 20 | cmo | |- mod |
|
| 21 | 19 11 20 | co | |- ( ( |_ ` ( ( b ^ -u k ) x. r ) ) mod b ) |
| 22 | 3 5 4 9 21 | cmpo | |- ( k e. ZZ , r e. ( 0 [,) +oo ) |-> ( ( |_ ` ( ( b ^ -u k ) x. r ) ) mod b ) ) |
| 23 | 1 2 22 | cmpt | |- ( b e. NN |-> ( k e. ZZ , r e. ( 0 [,) +oo ) |-> ( ( |_ ` ( ( b ^ -u k ) x. r ) ) mod b ) ) ) |
| 24 | 0 23 | wceq | |- digit = ( b e. NN |-> ( k e. ZZ , r e. ( 0 [,) +oo ) |-> ( ( |_ ` ( ( b ^ -u k ) x. r ) ) mod b ) ) ) |