Description: The digits of the fractional part of a nonnegative integer are 0. (Contributed by AV, 23-May-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | dignn0fr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id | |
|
2 | eldifi | |
|
3 | nn0re | |
|
4 | nn0ge0 | |
|
5 | elrege0 | |
|
6 | 3 4 5 | sylanbrc | |
7 | digval | |
|
8 | 1 2 6 7 | syl3an | |
9 | nnz | |
|
10 | eldif | |
|
11 | znnn0nn | |
|
12 | 10 11 | sylbi | |
13 | 12 | nnnn0d | |
14 | zexpcl | |
|
15 | 9 13 14 | syl2an | |
16 | 15 | 3adant3 | |
17 | nn0z | |
|
18 | 17 | 3ad2ant3 | |
19 | 16 18 | zmulcld | |
20 | flid | |
|
21 | 19 20 | syl | |
22 | 21 | oveq1d | |
23 | nnre | |
|
24 | reexpcl | |
|
25 | 23 13 24 | syl2an | |
26 | 25 | recnd | |
27 | 26 | 3adant3 | |
28 | nn0cn | |
|
29 | 28 | 3ad2ant3 | |
30 | nncn | |
|
31 | nnne0 | |
|
32 | 30 31 | jca | |
33 | 32 | 3ad2ant1 | |
34 | div23 | |
|
35 | 27 29 33 34 | syl3anc | |
36 | 30 | 3ad2ant1 | |
37 | 31 | 3ad2ant1 | |
38 | 12 | nnzd | |
39 | 38 | 3ad2ant2 | |
40 | 36 37 39 | expm1d | |
41 | 40 | eqcomd | |
42 | 41 | oveq1d | |
43 | 35 42 | eqtrd | |
44 | nnm1nn0 | |
|
45 | 12 44 | syl | |
46 | zexpcl | |
|
47 | 9 45 46 | syl2an | |
48 | 47 | 3adant3 | |
49 | 48 18 | zmulcld | |
50 | 43 49 | eqeltrd | |
51 | 25 | 3adant3 | |
52 | 3 | 3ad2ant3 | |
53 | 51 52 | remulcld | |
54 | nnrp | |
|
55 | 54 | 3ad2ant1 | |
56 | mod0 | |
|
57 | 53 55 56 | syl2anc | |
58 | 50 57 | mpbird | |
59 | 22 58 | eqtrd | |
60 | 8 59 | eqtrd | |