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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnre | |
|
2 | nnnn0 | |
|
3 | reexpcl | |
|
4 | 1 2 3 | syl2an | |
5 | remulcl | |
|
6 | 4 5 | stoic3 | |
7 | 6 | 3comr | |
8 | reflcl | |
|
9 | 7 8 | syl | |
10 | nnrp | |
|
11 | 10 | 3ad2ant2 | |
12 | modval | |
|
13 | 9 11 12 | syl2anc | |
14 | simp2 | |
|
15 | fldiv | |
|
16 | 7 14 15 | syl2anc | |
17 | nncn | |
|
18 | expcl | |
|
19 | 17 2 18 | syl2an | |
20 | 19 | 3adant1 | |
21 | recn | |
|
22 | 21 | 3ad2ant1 | |
23 | nnne0 | |
|
24 | 17 23 | jca | |
25 | 24 | 3ad2ant2 | |
26 | div23 | |
|
27 | 20 22 25 26 | syl3anc | |
28 | nnz | |
|
29 | expm1 | |
|
30 | 17 23 28 29 | syl2an3an | |
31 | 30 | 3adant1 | |
32 | 31 | oveq1d | |
33 | 27 32 | eqtr4d | |
34 | 33 | fveq2d | |
35 | 16 34 | eqtrd | |
36 | 35 | oveq2d | |
37 | 36 | oveq2d | |
38 | 13 37 | eqtrd | |