Metamath Proof Explorer

Theorem digit2

Description: Two ways to express the K th digit in the decimal (when base B = 1 0 ) expansion of a number A . K = 1 corresponds to the first digit after the decimal point. (Contributed by NM, 25-Dec-2008)

Ref Expression
Assertion digit2 
|- ( ( A e. RR /\ B e. NN /\ K e. NN ) -> ( ( |_ ` ( ( B ^ K ) x. A ) ) mod B ) = ( ( |_ ` ( ( B ^ K ) x. A ) ) - ( B x. ( |_ ` ( ( B ^ ( K - 1 ) ) x. A ) ) ) ) )

Proof

Step Hyp Ref Expression
1 nnre 
 |-  ( B e. NN -> B e. RR )
2 nnnn0 
 |-  ( K e. NN -> K e. NN0 )
3 reexpcl 
 |-  ( ( B e. RR /\ K e. NN0 ) -> ( B ^ K ) e. RR )
4 1 2 3 syl2an 
 |-  ( ( B e. NN /\ K e. NN ) -> ( B ^ K ) e. RR )
5 remulcl 
 |-  ( ( ( B ^ K ) e. RR /\ A e. RR ) -> ( ( B ^ K ) x. A ) e. RR )
6 4 5 stoic3 
 |-  ( ( B e. NN /\ K e. NN /\ A e. RR ) -> ( ( B ^ K ) x. A ) e. RR )
7 6 3comr 
 |-  ( ( A e. RR /\ B e. NN /\ K e. NN ) -> ( ( B ^ K ) x. A ) e. RR )
8 reflcl 
 |-  ( ( ( B ^ K ) x. A ) e. RR -> ( |_ ` ( ( B ^ K ) x. A ) ) e. RR )
9 7 8 syl 
 |-  ( ( A e. RR /\ B e. NN /\ K e. NN ) -> ( |_ ` ( ( B ^ K ) x. A ) ) e. RR )
10 nnrp 
 |-  ( B e. NN -> B e. RR+ )
11 10 3ad2ant2 
 |-  ( ( A e. RR /\ B e. NN /\ K e. NN ) -> B e. RR+ )
12 modval 
 |-  ( ( ( |_ ` ( ( B ^ K ) x. A ) ) e. RR /\ B e. RR+ ) -> ( ( |_ ` ( ( B ^ K ) x. A ) ) mod B ) = ( ( |_ ` ( ( B ^ K ) x. A ) ) - ( B x. ( |_ ` ( ( |_ ` ( ( B ^ K ) x. A ) ) / B ) ) ) ) )
13 9 11 12 syl2anc 
 |-  ( ( A e. RR /\ B e. NN /\ K e. NN ) -> ( ( |_ ` ( ( B ^ K ) x. A ) ) mod B ) = ( ( |_ ` ( ( B ^ K ) x. A ) ) - ( B x. ( |_ ` ( ( |_ ` ( ( B ^ K ) x. A ) ) / B ) ) ) ) )
14 simp2 
 |-  ( ( A e. RR /\ B e. NN /\ K e. NN ) -> B e. NN )
15 fldiv 
 |-  ( ( ( ( B ^ K ) x. A ) e. RR /\ B e. NN ) -> ( |_ ` ( ( |_ ` ( ( B ^ K ) x. A ) ) / B ) ) = ( |_ ` ( ( ( B ^ K ) x. A ) / B ) ) )
16 7 14 15 syl2anc 
 |-  ( ( A e. RR /\ B e. NN /\ K e. NN ) -> ( |_ ` ( ( |_ ` ( ( B ^ K ) x. A ) ) / B ) ) = ( |_ ` ( ( ( B ^ K ) x. A ) / B ) ) )
17 nncn 
 |-  ( B e. NN -> B e. CC )
18 expcl 
 |-  ( ( B e. CC /\ K e. NN0 ) -> ( B ^ K ) e. CC )
19 17 2 18 syl2an 
 |-  ( ( B e. NN /\ K e. NN ) -> ( B ^ K ) e. CC )
20 19 3adant1 
 |-  ( ( A e. RR /\ B e. NN /\ K e. NN ) -> ( B ^ K ) e. CC )
21 recn 
 |-  ( A e. RR -> A e. CC )
22 21 3ad2ant1 
 |-  ( ( A e. RR /\ B e. NN /\ K e. NN ) -> A e. CC )
23 nnne0 
 |-  ( B e. NN -> B =/= 0 )
24 17 23 jca 
 |-  ( B e. NN -> ( B e. CC /\ B =/= 0 ) )
25 24 3ad2ant2 
 |-  ( ( A e. RR /\ B e. NN /\ K e. NN ) -> ( B e. CC /\ B =/= 0 ) )
26 div23 
 |-  ( ( ( B ^ K ) e. CC /\ A e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( ( B ^ K ) x. A ) / B ) = ( ( ( B ^ K ) / B ) x. A ) )
27 20 22 25 26 syl3anc 
 |-  ( ( A e. RR /\ B e. NN /\ K e. NN ) -> ( ( ( B ^ K ) x. A ) / B ) = ( ( ( B ^ K ) / B ) x. A ) )
28 nnz 
 |-  ( K e. NN -> K e. ZZ )
29 expm1 
 |-  ( ( B e. CC /\ B =/= 0 /\ K e. ZZ ) -> ( B ^ ( K - 1 ) ) = ( ( B ^ K ) / B ) )
30 17 23 28 29 syl2an3an 
 |-  ( ( B e. NN /\ K e. NN ) -> ( B ^ ( K - 1 ) ) = ( ( B ^ K ) / B ) )
31 30 3adant1 
 |-  ( ( A e. RR /\ B e. NN /\ K e. NN ) -> ( B ^ ( K - 1 ) ) = ( ( B ^ K ) / B ) )
32 31 oveq1d 
 |-  ( ( A e. RR /\ B e. NN /\ K e. NN ) -> ( ( B ^ ( K - 1 ) ) x. A ) = ( ( ( B ^ K ) / B ) x. A ) )
33 27 32 eqtr4d 
 |-  ( ( A e. RR /\ B e. NN /\ K e. NN ) -> ( ( ( B ^ K ) x. A ) / B ) = ( ( B ^ ( K - 1 ) ) x. A ) )
34 33 fveq2d 
 |-  ( ( A e. RR /\ B e. NN /\ K e. NN ) -> ( |_ ` ( ( ( B ^ K ) x. A ) / B ) ) = ( |_ ` ( ( B ^ ( K - 1 ) ) x. A ) ) )
35 16 34 eqtrd 
 |-  ( ( A e. RR /\ B e. NN /\ K e. NN ) -> ( |_ ` ( ( |_ ` ( ( B ^ K ) x. A ) ) / B ) ) = ( |_ ` ( ( B ^ ( K - 1 ) ) x. A ) ) )
36 35 oveq2d 
 |-  ( ( A e. RR /\ B e. NN /\ K e. NN ) -> ( B x. ( |_ ` ( ( |_ ` ( ( B ^ K ) x. A ) ) / B ) ) ) = ( B x. ( |_ ` ( ( B ^ ( K - 1 ) ) x. A ) ) ) )
37 36 oveq2d 
 |-  ( ( A e. RR /\ B e. NN /\ K e. NN ) -> ( ( |_ ` ( ( B ^ K ) x. A ) ) - ( B x. ( |_ ` ( ( |_ ` ( ( B ^ K ) x. A ) ) / B ) ) ) ) = ( ( |_ ` ( ( B ^ K ) x. A ) ) - ( B x. ( |_ ` ( ( B ^ ( K - 1 ) ) x. A ) ) ) ) )
38 13 37 eqtrd 
 |-  ( ( A e. RR /\ B e. NN /\ K e. NN ) -> ( ( |_ ` ( ( B ^ K ) x. A ) ) mod B ) = ( ( |_ ` ( ( B ^ K ) x. A ) ) - ( B x. ( |_ ` ( ( B ^ ( K - 1 ) ) x. A ) ) ) ) )