Metamath Proof Explorer

Theorem digval

Description: 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 digval 
|- ( ( B e. NN /\ K e. ZZ /\ R e. ( 0 [,) +oo ) ) -> ( K ( digit ` B ) R ) = ( ( |_ ` ( ( B ^ -u K ) x. R ) ) mod B ) )

Proof

Step Hyp Ref Expression
1 digfval 
 |-  ( B e. NN -> ( digit ` B ) = ( k e. ZZ , r e. ( 0 [,) +oo ) |-> ( ( |_ ` ( ( B ^ -u k ) x. r ) ) mod B ) ) )
2 1 3ad2ant1 
 |-  ( ( B e. NN /\ K e. ZZ /\ R e. ( 0 [,) +oo ) ) -> ( digit ` B ) = ( k e. ZZ , r e. ( 0 [,) +oo ) |-> ( ( |_ ` ( ( B ^ -u k ) x. r ) ) mod B ) ) )
3 negeq 
 |-  ( k = K -> -u k = -u K )
4 3 oveq2d 
 |-  ( k = K -> ( B ^ -u k ) = ( B ^ -u K ) )
5 4 adantr 
 |-  ( ( k = K /\ r = R ) -> ( B ^ -u k ) = ( B ^ -u K ) )
6 simpr 
 |-  ( ( k = K /\ r = R ) -> r = R )
7 5 6 oveq12d 
 |-  ( ( k = K /\ r = R ) -> ( ( B ^ -u k ) x. r ) = ( ( B ^ -u K ) x. R ) )
8 7 fveq2d 
 |-  ( ( k = K /\ r = R ) -> ( |_ ` ( ( B ^ -u k ) x. r ) ) = ( |_ ` ( ( B ^ -u K ) x. R ) ) )
9 8 oveq1d 
 |-  ( ( k = K /\ r = R ) -> ( ( |_ ` ( ( B ^ -u k ) x. r ) ) mod B ) = ( ( |_ ` ( ( B ^ -u K ) x. R ) ) mod B ) )
10 9 adantl 
 |-  ( ( ( B e. NN /\ K e. ZZ /\ R e. ( 0 [,) +oo ) ) /\ ( k = K /\ r = R ) ) -> ( ( |_ ` ( ( B ^ -u k ) x. r ) ) mod B ) = ( ( |_ ` ( ( B ^ -u K ) x. R ) ) mod B ) )
11 simp2 
 |-  ( ( B e. NN /\ K e. ZZ /\ R e. ( 0 [,) +oo ) ) -> K e. ZZ )
12 simp3 
 |-  ( ( B e. NN /\ K e. ZZ /\ R e. ( 0 [,) +oo ) ) -> R e. ( 0 [,) +oo ) )
13 ovexd 
 |-  ( ( B e. NN /\ K e. ZZ /\ R e. ( 0 [,) +oo ) ) -> ( ( |_ ` ( ( B ^ -u K ) x. R ) ) mod B ) e. _V )
14 2 10 11 12 13 ovmpod 
 |-  ( ( B e. NN /\ K e. ZZ /\ R e. ( 0 [,) +oo ) ) -> ( K ( digit ` B ) R ) = ( ( |_ ` ( ( B ^ -u K ) x. R ) ) mod B ) )