Metamath Proof Explorer

Theorem nn0digval

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 nn0digval 
|- ( ( B e. NN /\ K e. NN0 /\ R e. ( 0 [,) +oo ) ) -> ( K ( digit ` B ) R ) = ( ( |_ ` ( R / ( B ^ K ) ) ) mod B ) )

Proof

Step Hyp Ref Expression
1 nn0z 
 |-  ( K e. NN0 -> K e. ZZ )
2 digval 
 |-  ( ( B e. NN /\ K e. ZZ /\ R e. ( 0 [,) +oo ) ) -> ( K ( digit ` B ) R ) = ( ( |_ ` ( ( B ^ -u K ) x. R ) ) mod B ) )
3 1 2 syl3an2 
 |-  ( ( B e. NN /\ K e. NN0 /\ R e. ( 0 [,) +oo ) ) -> ( K ( digit ` B ) R ) = ( ( |_ ` ( ( B ^ -u K ) x. R ) ) mod B ) )
4 nncn 
 |-  ( B e. NN -> B e. CC )
5 4 anim1i 
 |-  ( ( B e. NN /\ K e. NN0 ) -> ( B e. CC /\ K e. NN0 ) )
6 expneg 
 |-  ( ( B e. CC /\ K e. NN0 ) -> ( B ^ -u K ) = ( 1 / ( B ^ K ) ) )
7 5 6 syl 
 |-  ( ( B e. NN /\ K e. NN0 ) -> ( B ^ -u K ) = ( 1 / ( B ^ K ) ) )
8 7 3adant3 
 |-  ( ( B e. NN /\ K e. NN0 /\ R e. ( 0 [,) +oo ) ) -> ( B ^ -u K ) = ( 1 / ( B ^ K ) ) )
9 8 oveq1d 
 |-  ( ( B e. NN /\ K e. NN0 /\ R e. ( 0 [,) +oo ) ) -> ( ( B ^ -u K ) x. R ) = ( ( 1 / ( B ^ K ) ) x. R ) )
10 elrege0 
 |-  ( R e. ( 0 [,) +oo ) <-> ( R e. RR /\ 0 <_ R ) )
11 recn 
 |-  ( R e. RR -> R e. CC )
12 11 adantr 
 |-  ( ( R e. RR /\ 0 <_ R ) -> R e. CC )
13 10 12 sylbi 
 |-  ( R e. ( 0 [,) +oo ) -> R e. CC )
14 13 3ad2ant3 
 |-  ( ( B e. NN /\ K e. NN0 /\ R e. ( 0 [,) +oo ) ) -> R e. CC )
15 5 3adant3 
 |-  ( ( B e. NN /\ K e. NN0 /\ R e. ( 0 [,) +oo ) ) -> ( B e. CC /\ K e. NN0 ) )
16 expcl 
 |-  ( ( B e. CC /\ K e. NN0 ) -> ( B ^ K ) e. CC )
17 15 16 syl 
 |-  ( ( B e. NN /\ K e. NN0 /\ R e. ( 0 [,) +oo ) ) -> ( B ^ K ) e. CC )
18 4 3ad2ant1 
 |-  ( ( B e. NN /\ K e. NN0 /\ R e. ( 0 [,) +oo ) ) -> B e. CC )
19 nnne0 
 |-  ( B e. NN -> B =/= 0 )
20 19 3ad2ant1 
 |-  ( ( B e. NN /\ K e. NN0 /\ R e. ( 0 [,) +oo ) ) -> B =/= 0 )
21 1 3ad2ant2 
 |-  ( ( B e. NN /\ K e. NN0 /\ R e. ( 0 [,) +oo ) ) -> K e. ZZ )
22 18 20 21 expne0d 
 |-  ( ( B e. NN /\ K e. NN0 /\ R e. ( 0 [,) +oo ) ) -> ( B ^ K ) =/= 0 )
23 14 17 22 divrec2d 
 |-  ( ( B e. NN /\ K e. NN0 /\ R e. ( 0 [,) +oo ) ) -> ( R / ( B ^ K ) ) = ( ( 1 / ( B ^ K ) ) x. R ) )
24 9 23 eqtr4d 
 |-  ( ( B e. NN /\ K e. NN0 /\ R e. ( 0 [,) +oo ) ) -> ( ( B ^ -u K ) x. R ) = ( R / ( B ^ K ) ) )
25 24 fveq2d 
 |-  ( ( B e. NN /\ K e. NN0 /\ R e. ( 0 [,) +oo ) ) -> ( |_ ` ( ( B ^ -u K ) x. R ) ) = ( |_ ` ( R / ( B ^ K ) ) ) )
26 25 oveq1d 
 |-  ( ( B e. NN /\ K e. NN0 /\ R e. ( 0 [,) +oo ) ) -> ( ( |_ ` ( ( B ^ -u K ) x. R ) ) mod B ) = ( ( |_ ` ( R / ( B ^ K ) ) ) mod B ) )
27 3 26 eqtrd 
 |-  ( ( B e. NN /\ K e. NN0 /\ R e. ( 0 [,) +oo ) ) -> ( K ( digit ` B ) R ) = ( ( |_ ` ( R / ( B ^ K ) ) ) mod B ) )