Metamath Proof Explorer


Theorem dignn0fr

Description: The digits of the fractional part of a nonnegative integer are 0. (Contributed by AV, 23-May-2020)

Ref Expression
Assertion dignn0fr BK0N0KdigitBN=0

Proof

Step Hyp Ref Expression
1 id BB
2 eldifi K0K
3 nn0re N0N
4 nn0ge0 N00N
5 elrege0 N0+∞N0N
6 3 4 5 sylanbrc N0N0+∞
7 digval BKN0+∞KdigitBN=BK NmodB
8 1 2 6 7 syl3an BK0N0KdigitBN=BK NmodB
9 nnz BB
10 eldif K0K¬K0
11 znnn0nn K¬K0K
12 10 11 sylbi K0K
13 12 nnnn0d K0K0
14 zexpcl BK0BK
15 9 13 14 syl2an BK0BK
16 15 3adant3 BK0N0BK
17 nn0z N0N
18 17 3ad2ant3 BK0N0N
19 16 18 zmulcld BK0N0BK N
20 flid BK NBK N=BK N
21 19 20 syl BK0N0BK N=BK N
22 21 oveq1d BK0N0BK NmodB=BK NmodB
23 nnre BB
24 reexpcl BK0BK
25 23 13 24 syl2an BK0BK
26 25 recnd BK0BK
27 26 3adant3 BK0N0BK
28 nn0cn N0N
29 28 3ad2ant3 BK0N0N
30 nncn BB
31 nnne0 BB0
32 30 31 jca BBB0
33 32 3ad2ant1 BK0N0BB0
34 div23 BKNBB0BK NB=BKB N
35 27 29 33 34 syl3anc BK0N0BK NB=BKB N
36 30 3ad2ant1 BK0N0B
37 31 3ad2ant1 BK0N0B0
38 12 nnzd K0K
39 38 3ad2ant2 BK0N0K
40 36 37 39 expm1d BK0N0B-K-1=BKB
41 40 eqcomd BK0N0BKB=B-K-1
42 41 oveq1d BK0N0BKB N=B-K-1 N
43 35 42 eqtrd BK0N0BK NB=B-K-1 N
44 nnm1nn0 K-K-10
45 12 44 syl K0-K-10
46 zexpcl B-K-10B-K-1
47 9 45 46 syl2an BK0B-K-1
48 47 3adant3 BK0N0B-K-1
49 48 18 zmulcld BK0N0B-K-1 N
50 43 49 eqeltrd BK0N0BK NB
51 25 3adant3 BK0N0BK
52 3 3ad2ant3 BK0N0N
53 51 52 remulcld BK0N0BK N
54 nnrp BB+
55 54 3ad2ant1 BK0N0B+
56 mod0 BK NB+BK NmodB=0BK NB
57 53 55 56 syl2anc BK0N0BK NmodB=0BK NB
58 50 57 mpbird BK0N0BK NmodB=0
59 22 58 eqtrd BK0N0BK NmodB=0
60 8 59 eqtrd BK0N0KdigitBN=0