Metamath Proof Explorer

Theorem digfval

Description: Operation to obtain the k th digit of a nonnegative real number r in the positional system with base B . (Contributed by AV, 23-May-2020)

Ref Expression
Assertion digfval 
|- ( B e. NN -> ( digit ` B ) = ( k e. ZZ , r e. ( 0 [,) +oo ) |-> ( ( |_ ` ( ( B ^ -u k ) x. r ) ) mod B ) ) )

Proof

Step Hyp Ref Expression
1 df-dig 
 |-  digit = ( b e. NN |-> ( k e. ZZ , r e. ( 0 [,) +oo ) |-> ( ( |_ ` ( ( b ^ -u k ) x. r ) ) mod b ) ) )
2 oveq1 
 |-  ( b = B -> ( b ^ -u k ) = ( B ^ -u k ) )
3 2 fvoveq1d 
 |-  ( b = B -> ( |_ ` ( ( b ^ -u k ) x. r ) ) = ( |_ ` ( ( B ^ -u k ) x. r ) ) )
4 id 
 |-  ( b = B -> b = B )
5 3 4 oveq12d 
 |-  ( b = B -> ( ( |_ ` ( ( b ^ -u k ) x. r ) ) mod b ) = ( ( |_ ` ( ( B ^ -u k ) x. r ) ) mod B ) )
6 5 mpoeq3dv 
 |-  ( b = B -> ( k e. ZZ , r e. ( 0 [,) +oo ) |-> ( ( |_ ` ( ( b ^ -u k ) x. r ) ) mod b ) ) = ( k e. ZZ , r e. ( 0 [,) +oo ) |-> ( ( |_ ` ( ( B ^ -u k ) x. r ) ) mod B ) ) )
7 id 
 |-  ( B e. NN -> B e. NN )
8 zex 
 |-  ZZ e. _V
9 ovex 
 |-  ( 0 [,) +oo ) e. _V
10 8 9 pm3.2i 
 |-  ( ZZ e. _V /\ ( 0 [,) +oo ) e. _V )
11 eqid 
 |-  ( k e. ZZ , r e. ( 0 [,) +oo ) |-> ( ( |_ ` ( ( B ^ -u k ) x. r ) ) mod B ) ) = ( k e. ZZ , r e. ( 0 [,) +oo ) |-> ( ( |_ ` ( ( B ^ -u k ) x. r ) ) mod B ) )
12 11 mpoexg 
 |-  ( ( ZZ e. _V /\ ( 0 [,) +oo ) e. _V ) -> ( k e. ZZ , r e. ( 0 [,) +oo ) |-> ( ( |_ ` ( ( B ^ -u k ) x. r ) ) mod B ) ) e. _V )
13 10 12 mp1i 
 |-  ( B e. NN -> ( k e. ZZ , r e. ( 0 [,) +oo ) |-> ( ( |_ ` ( ( B ^ -u k ) x. r ) ) mod B ) ) e. _V )
14 1 6 7 13 fvmptd3 
 |-  ( B e. NN -> ( digit ` B ) = ( k e. ZZ , r e. ( 0 [,) +oo ) |-> ( ( |_ ` ( ( B ^ -u k ) x. r ) ) mod B ) ) )