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 ABKBKAmodB=BKABBK1A

Proof

Step Hyp Ref Expression
1 nnre BB
2 nnnn0 KK0
3 reexpcl BK0BK
4 1 2 3 syl2an BKBK
5 remulcl BKABKA
6 4 5 stoic3 BKABKA
7 6 3comr ABKBKA
8 reflcl BKABKA
9 7 8 syl ABKBKA
10 nnrp BB+
11 10 3ad2ant2 ABKB+
12 modval BKAB+BKAmodB=BKABBKAB
13 9 11 12 syl2anc ABKBKAmodB=BKABBKAB
14 simp2 ABKB
15 fldiv BKABBKAB=BKAB
16 7 14 15 syl2anc ABKBKAB=BKAB
17 nncn BB
18 expcl BK0BK
19 17 2 18 syl2an BKBK
20 19 3adant1 ABKBK
21 recn AA
22 21 3ad2ant1 ABKA
23 nnne0 BB0
24 17 23 jca BBB0
25 24 3ad2ant2 ABKBB0
26 div23 BKABB0BKAB=BKBA
27 20 22 25 26 syl3anc ABKBKAB=BKBA
28 nnz KK
29 expm1 BB0KBK1=BKB
30 17 23 28 29 syl2an3an BKBK1=BKB
31 30 3adant1 ABKBK1=BKB
32 31 oveq1d ABKBK1A=BKBA
33 27 32 eqtr4d ABKBKAB=BK1A
34 33 fveq2d ABKBKAB=BK1A
35 16 34 eqtrd ABKBKAB=BK1A
36 35 oveq2d ABKBBKAB=BBK1A
37 36 oveq2d ABKBKABBKAB=BKABBK1A
38 13 37 eqtrd ABKBKAmodB=BKABBK1A