Metamath Proof Explorer

Theorem digit1

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

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

Proof

Step Hyp Ref Expression
1 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 ) ) ) ) )
2 1 3coml 
 |-  ( ( B e. NN /\ K e. NN /\ A e. RR ) -> ( ( |_ ` ( ( B ^ K ) x. A ) ) mod B ) = ( ( |_ ` ( ( B ^ K ) x. A ) ) - ( B x. ( |_ ` ( ( B ^ ( K - 1 ) ) x. A ) ) ) ) )
3 2 3expa 
 |-  ( ( ( B e. NN /\ K e. NN ) /\ A e. RR ) -> ( ( |_ ` ( ( B ^ K ) x. A ) ) mod B ) = ( ( |_ ` ( ( B ^ K ) x. A ) ) - ( B x. ( |_ ` ( ( B ^ ( K - 1 ) ) x. A ) ) ) ) )
4 3 oveq1d 
 |-  ( ( ( B e. NN /\ K e. NN ) /\ A e. RR ) -> ( ( ( |_ ` ( ( B ^ K ) x. A ) ) mod B ) mod ( B ^ K ) ) = ( ( ( |_ ` ( ( B ^ K ) x. A ) ) - ( B x. ( |_ ` ( ( B ^ ( K - 1 ) ) x. A ) ) ) ) mod ( B ^ K ) ) )
5 nnre 
 |-  ( B e. NN -> B e. RR )
6 nnnn0 
 |-  ( K e. NN -> K e. NN0 )
7 reexpcl 
 |-  ( ( B e. RR /\ K e. NN0 ) -> ( B ^ K ) e. RR )
8 5 6 7 syl2an 
 |-  ( ( B e. NN /\ K e. NN ) -> ( B ^ K ) e. RR )
9 remulcl 
 |-  ( ( ( B ^ K ) e. RR /\ A e. RR ) -> ( ( B ^ K ) x. A ) e. RR )
10 8 9 sylan 
 |-  ( ( ( B e. NN /\ K e. NN ) /\ A e. RR ) -> ( ( B ^ K ) x. A ) e. RR )
11 reflcl 
 |-  ( ( ( B ^ K ) x. A ) e. RR -> ( |_ ` ( ( B ^ K ) x. A ) ) e. RR )
12 10 11 syl 
 |-  ( ( ( B e. NN /\ K e. NN ) /\ A e. RR ) -> ( |_ ` ( ( B ^ K ) x. A ) ) e. RR )
13 nnrp 
 |-  ( B e. NN -> B e. RR+ )
14 13 ad2antrr 
 |-  ( ( ( B e. NN /\ K e. NN ) /\ A e. RR ) -> B e. RR+ )
15 12 14 modcld 
 |-  ( ( ( B e. NN /\ K e. NN ) /\ A e. RR ) -> ( ( |_ ` ( ( B ^ K ) x. A ) ) mod B ) e. RR )
16 nnexpcl 
 |-  ( ( B e. NN /\ K e. NN0 ) -> ( B ^ K ) e. NN )
17 6 16 sylan2 
 |-  ( ( B e. NN /\ K e. NN ) -> ( B ^ K ) e. NN )
18 17 nnrpd 
 |-  ( ( B e. NN /\ K e. NN ) -> ( B ^ K ) e. RR+ )
19 18 adantr 
 |-  ( ( ( B e. NN /\ K e. NN ) /\ A e. RR ) -> ( B ^ K ) e. RR+ )
20 modge0 
 |-  ( ( ( |_ ` ( ( B ^ K ) x. A ) ) e. RR /\ B e. RR+ ) -> 0 <_ ( ( |_ ` ( ( B ^ K ) x. A ) ) mod B ) )
21 12 14 20 syl2anc 
 |-  ( ( ( B e. NN /\ K e. NN ) /\ A e. RR ) -> 0 <_ ( ( |_ ` ( ( B ^ K ) x. A ) ) mod B ) )
22 5 ad2antrr 
 |-  ( ( ( B e. NN /\ K e. NN ) /\ A e. RR ) -> B e. RR )
23 8 adantr 
 |-  ( ( ( B e. NN /\ K e. NN ) /\ A e. RR ) -> ( B ^ K ) e. RR )
24 modlt 
 |-  ( ( ( |_ ` ( ( B ^ K ) x. A ) ) e. RR /\ B e. RR+ ) -> ( ( |_ ` ( ( B ^ K ) x. A ) ) mod B ) < B )
25 12 14 24 syl2anc 
 |-  ( ( ( B e. NN /\ K e. NN ) /\ A e. RR ) -> ( ( |_ ` ( ( B ^ K ) x. A ) ) mod B ) < B )
26 nncn 
 |-  ( B e. NN -> B e. CC )
27 exp1 
 |-  ( B e. CC -> ( B ^ 1 ) = B )
28 26 27 syl 
 |-  ( B e. NN -> ( B ^ 1 ) = B )
29 28 adantr 
 |-  ( ( B e. NN /\ K e. NN ) -> ( B ^ 1 ) = B )
30 5 adantr 
 |-  ( ( B e. NN /\ K e. NN ) -> B e. RR )
31 nnge1 
 |-  ( B e. NN -> 1 <_ B )
32 31 adantr 
 |-  ( ( B e. NN /\ K e. NN ) -> 1 <_ B )
33 simpr 
 |-  ( ( B e. NN /\ K e. NN ) -> K e. NN )
34 nnuz 
 |-  NN = ( ZZ>= ` 1 )
35 33 34 eleqtrdi 
 |-  ( ( B e. NN /\ K e. NN ) -> K e. ( ZZ>= ` 1 ) )
36 leexp2a 
 |-  ( ( B e. RR /\ 1 <_ B /\ K e. ( ZZ>= ` 1 ) ) -> ( B ^ 1 ) <_ ( B ^ K ) )
37 30 32 35 36 syl3anc 
 |-  ( ( B e. NN /\ K e. NN ) -> ( B ^ 1 ) <_ ( B ^ K ) )
38 29 37 eqbrtrrd 
 |-  ( ( B e. NN /\ K e. NN ) -> B <_ ( B ^ K ) )
39 38 adantr 
 |-  ( ( ( B e. NN /\ K e. NN ) /\ A e. RR ) -> B <_ ( B ^ K ) )
40 15 22 23 25 39 ltletrd 
 |-  ( ( ( B e. NN /\ K e. NN ) /\ A e. RR ) -> ( ( |_ ` ( ( B ^ K ) x. A ) ) mod B ) < ( B ^ K ) )
41 modid 
 |-  ( ( ( ( ( |_ ` ( ( B ^ K ) x. A ) ) mod B ) e. RR /\ ( B ^ K ) e. RR+ ) /\ ( 0 <_ ( ( |_ ` ( ( B ^ K ) x. A ) ) mod B ) /\ ( ( |_ ` ( ( B ^ K ) x. A ) ) mod B ) < ( B ^ K ) ) ) -> ( ( ( |_ ` ( ( B ^ K ) x. A ) ) mod B ) mod ( B ^ K ) ) = ( ( |_ ` ( ( B ^ K ) x. A ) ) mod B ) )
42 15 19 21 40 41 syl22anc 
 |-  ( ( ( B e. NN /\ K e. NN ) /\ A e. RR ) -> ( ( ( |_ ` ( ( B ^ K ) x. A ) ) mod B ) mod ( B ^ K ) ) = ( ( |_ ` ( ( B ^ K ) x. A ) ) mod B ) )
43 simpll 
 |-  ( ( ( B e. NN /\ K e. NN ) /\ A e. RR ) -> B e. NN )
44 nnm1nn0 
 |-  ( K e. NN -> ( K - 1 ) e. NN0 )
45 reexpcl 
 |-  ( ( B e. RR /\ ( K - 1 ) e. NN0 ) -> ( B ^ ( K - 1 ) ) e. RR )
46 5 44 45 syl2an 
 |-  ( ( B e. NN /\ K e. NN ) -> ( B ^ ( K - 1 ) ) e. RR )
47 remulcl 
 |-  ( ( ( B ^ ( K - 1 ) ) e. RR /\ A e. RR ) -> ( ( B ^ ( K - 1 ) ) x. A ) e. RR )
48 46 47 sylan 
 |-  ( ( ( B e. NN /\ K e. NN ) /\ A e. RR ) -> ( ( B ^ ( K - 1 ) ) x. A ) e. RR )
49 nnexpcl 
 |-  ( ( B e. NN /\ ( K - 1 ) e. NN0 ) -> ( B ^ ( K - 1 ) ) e. NN )
50 44 49 sylan2 
 |-  ( ( B e. NN /\ K e. NN ) -> ( B ^ ( K - 1 ) ) e. NN )
51 50 adantr 
 |-  ( ( ( B e. NN /\ K e. NN ) /\ A e. RR ) -> ( B ^ ( K - 1 ) ) e. NN )
52 modmulnn 
 |-  ( ( B e. NN /\ ( ( B ^ ( K - 1 ) ) x. A ) e. RR /\ ( B ^ ( K - 1 ) ) e. NN ) -> ( ( B x. ( |_ ` ( ( B ^ ( K - 1 ) ) x. A ) ) ) mod ( B x. ( B ^ ( K - 1 ) ) ) ) <_ ( ( |_ ` ( B x. ( ( B ^ ( K - 1 ) ) x. A ) ) ) mod ( B x. ( B ^ ( K - 1 ) ) ) ) )
53 43 48 51 52 syl3anc 
 |-  ( ( ( B e. NN /\ K e. NN ) /\ A e. RR ) -> ( ( B x. ( |_ ` ( ( B ^ ( K - 1 ) ) x. A ) ) ) mod ( B x. ( B ^ ( K - 1 ) ) ) ) <_ ( ( |_ ` ( B x. ( ( B ^ ( K - 1 ) ) x. A ) ) ) mod ( B x. ( B ^ ( K - 1 ) ) ) ) )
54 expm1t 
 |-  ( ( B e. CC /\ K e. NN ) -> ( B ^ K ) = ( ( B ^ ( K - 1 ) ) x. B ) )
55 expcl 
 |-  ( ( B e. CC /\ ( K - 1 ) e. NN0 ) -> ( B ^ ( K - 1 ) ) e. CC )
56 44 55 sylan2 
 |-  ( ( B e. CC /\ K e. NN ) -> ( B ^ ( K - 1 ) ) e. CC )
57 simpl 
 |-  ( ( B e. CC /\ K e. NN ) -> B e. CC )
58 56 57 mulcomd 
 |-  ( ( B e. CC /\ K e. NN ) -> ( ( B ^ ( K - 1 ) ) x. B ) = ( B x. ( B ^ ( K - 1 ) ) ) )
59 54 58 eqtrd 
 |-  ( ( B e. CC /\ K e. NN ) -> ( B ^ K ) = ( B x. ( B ^ ( K - 1 ) ) ) )
60 26 59 sylan 
 |-  ( ( B e. NN /\ K e. NN ) -> ( B ^ K ) = ( B x. ( B ^ ( K - 1 ) ) ) )
61 60 adantr 
 |-  ( ( ( B e. NN /\ K e. NN ) /\ A e. RR ) -> ( B ^ K ) = ( B x. ( B ^ ( K - 1 ) ) ) )
62 61 oveq2d 
 |-  ( ( ( B e. NN /\ K e. NN ) /\ A e. RR ) -> ( ( B x. ( |_ ` ( ( B ^ ( K - 1 ) ) x. A ) ) ) mod ( B ^ K ) ) = ( ( B x. ( |_ ` ( ( B ^ ( K - 1 ) ) x. A ) ) ) mod ( B x. ( B ^ ( K - 1 ) ) ) ) )
63 61 oveq1d 
 |-  ( ( ( B e. NN /\ K e. NN ) /\ A e. RR ) -> ( ( B ^ K ) x. A ) = ( ( B x. ( B ^ ( K - 1 ) ) ) x. A ) )
64 26 ad2antrr 
 |-  ( ( ( B e. NN /\ K e. NN ) /\ A e. RR ) -> B e. CC )
65 26 44 55 syl2an 
 |-  ( ( B e. NN /\ K e. NN ) -> ( B ^ ( K - 1 ) ) e. CC )
66 65 adantr 
 |-  ( ( ( B e. NN /\ K e. NN ) /\ A e. RR ) -> ( B ^ ( K - 1 ) ) e. CC )
67 recn 
 |-  ( A e. RR -> A e. CC )
68 67 adantl 
 |-  ( ( ( B e. NN /\ K e. NN ) /\ A e. RR ) -> A e. CC )
69 64 66 68 mulassd 
 |-  ( ( ( B e. NN /\ K e. NN ) /\ A e. RR ) -> ( ( B x. ( B ^ ( K - 1 ) ) ) x. A ) = ( B x. ( ( B ^ ( K - 1 ) ) x. A ) ) )
70 63 69 eqtrd 
 |-  ( ( ( B e. NN /\ K e. NN ) /\ A e. RR ) -> ( ( B ^ K ) x. A ) = ( B x. ( ( B ^ ( K - 1 ) ) x. A ) ) )
71 70 fveq2d 
 |-  ( ( ( B e. NN /\ K e. NN ) /\ A e. RR ) -> ( |_ ` ( ( B ^ K ) x. A ) ) = ( |_ ` ( B x. ( ( B ^ ( K - 1 ) ) x. A ) ) ) )
72 71 61 oveq12d 
 |-  ( ( ( B e. NN /\ K e. NN ) /\ A e. RR ) -> ( ( |_ ` ( ( B ^ K ) x. A ) ) mod ( B ^ K ) ) = ( ( |_ ` ( B x. ( ( B ^ ( K - 1 ) ) x. A ) ) ) mod ( B x. ( B ^ ( K - 1 ) ) ) ) )
73 53 62 72 3brtr4d 
 |-  ( ( ( B e. NN /\ K e. NN ) /\ A e. RR ) -> ( ( B x. ( |_ ` ( ( B ^ ( K - 1 ) ) x. A ) ) ) mod ( B ^ K ) ) <_ ( ( |_ ` ( ( B ^ K ) x. A ) ) mod ( B ^ K ) ) )
74 reflcl 
 |-  ( ( ( B ^ ( K - 1 ) ) x. A ) e. RR -> ( |_ ` ( ( B ^ ( K - 1 ) ) x. A ) ) e. RR )
75 48 74 syl 
 |-  ( ( ( B e. NN /\ K e. NN ) /\ A e. RR ) -> ( |_ ` ( ( B ^ ( K - 1 ) ) x. A ) ) e. RR )
76 remulcl 
 |-  ( ( B e. RR /\ ( |_ ` ( ( B ^ ( K - 1 ) ) x. A ) ) e. RR ) -> ( B x. ( |_ ` ( ( B ^ ( K - 1 ) ) x. A ) ) ) e. RR )
77 22 75 76 syl2anc 
 |-  ( ( ( B e. NN /\ K e. NN ) /\ A e. RR ) -> ( B x. ( |_ ` ( ( B ^ ( K - 1 ) ) x. A ) ) ) e. RR )
78 modsubdir 
 |-  ( ( ( |_ ` ( ( B ^ K ) x. A ) ) e. RR /\ ( B x. ( |_ ` ( ( B ^ ( K - 1 ) ) x. A ) ) ) e. RR /\ ( B ^ K ) e. RR+ ) -> ( ( ( B x. ( |_ ` ( ( B ^ ( K - 1 ) ) x. A ) ) ) mod ( B ^ K ) ) <_ ( ( |_ ` ( ( B ^ K ) x. A ) ) mod ( B ^ K ) ) <-> ( ( ( |_ ` ( ( B ^ K ) x. A ) ) - ( B x. ( |_ ` ( ( B ^ ( K - 1 ) ) x. A ) ) ) ) mod ( B ^ K ) ) = ( ( ( |_ ` ( ( B ^ K ) x. A ) ) mod ( B ^ K ) ) - ( ( B x. ( |_ ` ( ( B ^ ( K - 1 ) ) x. A ) ) ) mod ( B ^ K ) ) ) ) )
79 12 77 19 78 syl3anc 
 |-  ( ( ( B e. NN /\ K e. NN ) /\ A e. RR ) -> ( ( ( B x. ( |_ ` ( ( B ^ ( K - 1 ) ) x. A ) ) ) mod ( B ^ K ) ) <_ ( ( |_ ` ( ( B ^ K ) x. A ) ) mod ( B ^ K ) ) <-> ( ( ( |_ ` ( ( B ^ K ) x. A ) ) - ( B x. ( |_ ` ( ( B ^ ( K - 1 ) ) x. A ) ) ) ) mod ( B ^ K ) ) = ( ( ( |_ ` ( ( B ^ K ) x. A ) ) mod ( B ^ K ) ) - ( ( B x. ( |_ ` ( ( B ^ ( K - 1 ) ) x. A ) ) ) mod ( B ^ K ) ) ) ) )
80 73 79 mpbid 
 |-  ( ( ( B e. NN /\ K e. NN ) /\ A e. RR ) -> ( ( ( |_ ` ( ( B ^ K ) x. A ) ) - ( B x. ( |_ ` ( ( B ^ ( K - 1 ) ) x. A ) ) ) ) mod ( B ^ K ) ) = ( ( ( |_ ` ( ( B ^ K ) x. A ) ) mod ( B ^ K ) ) - ( ( B x. ( |_ ` ( ( B ^ ( K - 1 ) ) x. A ) ) ) mod ( B ^ K ) ) ) )
81 4 42 80 3eqtr3d 
 |-  ( ( ( B e. NN /\ K e. NN ) /\ A e. RR ) -> ( ( |_ ` ( ( B ^ K ) x. A ) ) mod B ) = ( ( ( |_ ` ( ( B ^ K ) x. A ) ) mod ( B ^ K ) ) - ( ( B x. ( |_ ` ( ( B ^ ( K - 1 ) ) x. A ) ) ) mod ( B ^ K ) ) ) )
82 81 3impa 
 |-  ( ( B e. NN /\ K e. NN /\ A e. RR ) -> ( ( |_ ` ( ( B ^ K ) x. A ) ) mod B ) = ( ( ( |_ ` ( ( B ^ K ) x. A ) ) mod ( B ^ K ) ) - ( ( B x. ( |_ ` ( ( B ^ ( K - 1 ) ) x. A ) ) ) mod ( B ^ K ) ) ) )
83 82 3comr 
 |-  ( ( A e. RR /\ B e. NN /\ K e. NN ) -> ( ( |_ ` ( ( B ^ K ) x. A ) ) mod B ) = ( ( ( |_ ` ( ( B ^ K ) x. A ) ) mod ( B ^ K ) ) - ( ( B x. ( |_ ` ( ( B ^ ( K - 1 ) ) x. A ) ) ) mod ( B ^ K ) ) ) )