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 
|- ( ( B e. NN /\ K e. ( ZZ \ NN0 ) /\ N e. NN0 ) -> ( K ( digit ` B ) N ) = 0 )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( B e. NN -> B e. NN )
2 eldifi 
 |-  ( K e. ( ZZ \ NN0 ) -> K e. ZZ )
3 nn0re 
 |-  ( N e. NN0 -> N e. RR )
4 nn0ge0 
 |-  ( N e. NN0 -> 0 <_ N )
5 elrege0 
 |-  ( N e. ( 0 [,) +oo ) <-> ( N e. RR /\ 0 <_ N ) )
6 3 4 5 sylanbrc 
 |-  ( N e. NN0 -> N e. ( 0 [,) +oo ) )
7 digval 
 |-  ( ( B e. NN /\ K e. ZZ /\ N e. ( 0 [,) +oo ) ) -> ( K ( digit ` B ) N ) = ( ( |_ ` ( ( B ^ -u K ) x. N ) ) mod B ) )
8 1 2 6 7 syl3an 
 |-  ( ( B e. NN /\ K e. ( ZZ \ NN0 ) /\ N e. NN0 ) -> ( K ( digit ` B ) N ) = ( ( |_ ` ( ( B ^ -u K ) x. N ) ) mod B ) )
9 nnz 
 |-  ( B e. NN -> B e. ZZ )
10 eldif 
 |-  ( K e. ( ZZ \ NN0 ) <-> ( K e. ZZ /\ -. K e. NN0 ) )
11 znnn0nn 
 |-  ( ( K e. ZZ /\ -. K e. NN0 ) -> -u K e. NN )
12 10 11 sylbi 
 |-  ( K e. ( ZZ \ NN0 ) -> -u K e. NN )
13 12 nnnn0d 
 |-  ( K e. ( ZZ \ NN0 ) -> -u K e. NN0 )
14 zexpcl 
 |-  ( ( B e. ZZ /\ -u K e. NN0 ) -> ( B ^ -u K ) e. ZZ )
15 9 13 14 syl2an 
 |-  ( ( B e. NN /\ K e. ( ZZ \ NN0 ) ) -> ( B ^ -u K ) e. ZZ )
16 15 3adant3 
 |-  ( ( B e. NN /\ K e. ( ZZ \ NN0 ) /\ N e. NN0 ) -> ( B ^ -u K ) e. ZZ )
17 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
18 17 3ad2ant3 
 |-  ( ( B e. NN /\ K e. ( ZZ \ NN0 ) /\ N e. NN0 ) -> N e. ZZ )
19 16 18 zmulcld 
 |-  ( ( B e. NN /\ K e. ( ZZ \ NN0 ) /\ N e. NN0 ) -> ( ( B ^ -u K ) x. N ) e. ZZ )
20 flid 
 |-  ( ( ( B ^ -u K ) x. N ) e. ZZ -> ( |_ ` ( ( B ^ -u K ) x. N ) ) = ( ( B ^ -u K ) x. N ) )
21 19 20 syl 
 |-  ( ( B e. NN /\ K e. ( ZZ \ NN0 ) /\ N e. NN0 ) -> ( |_ ` ( ( B ^ -u K ) x. N ) ) = ( ( B ^ -u K ) x. N ) )
22 21 oveq1d 
 |-  ( ( B e. NN /\ K e. ( ZZ \ NN0 ) /\ N e. NN0 ) -> ( ( |_ ` ( ( B ^ -u K ) x. N ) ) mod B ) = ( ( ( B ^ -u K ) x. N ) mod B ) )
23 nnre 
 |-  ( B e. NN -> B e. RR )
24 reexpcl 
 |-  ( ( B e. RR /\ -u K e. NN0 ) -> ( B ^ -u K ) e. RR )
25 23 13 24 syl2an 
 |-  ( ( B e. NN /\ K e. ( ZZ \ NN0 ) ) -> ( B ^ -u K ) e. RR )
26 25 recnd 
 |-  ( ( B e. NN /\ K e. ( ZZ \ NN0 ) ) -> ( B ^ -u K ) e. CC )
27 26 3adant3 
 |-  ( ( B e. NN /\ K e. ( ZZ \ NN0 ) /\ N e. NN0 ) -> ( B ^ -u K ) e. CC )
28 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
29 28 3ad2ant3 
 |-  ( ( B e. NN /\ K e. ( ZZ \ NN0 ) /\ N e. NN0 ) -> N e. CC )
30 nncn 
 |-  ( B e. NN -> B e. CC )
31 nnne0 
 |-  ( B e. NN -> B =/= 0 )
32 30 31 jca 
 |-  ( B e. NN -> ( B e. CC /\ B =/= 0 ) )
33 32 3ad2ant1 
 |-  ( ( B e. NN /\ K e. ( ZZ \ NN0 ) /\ N e. NN0 ) -> ( B e. CC /\ B =/= 0 ) )
34 div23 
 |-  ( ( ( B ^ -u K ) e. CC /\ N e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( ( B ^ -u K ) x. N ) / B ) = ( ( ( B ^ -u K ) / B ) x. N ) )
35 27 29 33 34 syl3anc 
 |-  ( ( B e. NN /\ K e. ( ZZ \ NN0 ) /\ N e. NN0 ) -> ( ( ( B ^ -u K ) x. N ) / B ) = ( ( ( B ^ -u K ) / B ) x. N ) )
36 30 3ad2ant1 
 |-  ( ( B e. NN /\ K e. ( ZZ \ NN0 ) /\ N e. NN0 ) -> B e. CC )
37 31 3ad2ant1 
 |-  ( ( B e. NN /\ K e. ( ZZ \ NN0 ) /\ N e. NN0 ) -> B =/= 0 )
38 12 nnzd 
 |-  ( K e. ( ZZ \ NN0 ) -> -u K e. ZZ )
39 38 3ad2ant2 
 |-  ( ( B e. NN /\ K e. ( ZZ \ NN0 ) /\ N e. NN0 ) -> -u K e. ZZ )
40 36 37 39 expm1d 
 |-  ( ( B e. NN /\ K e. ( ZZ \ NN0 ) /\ N e. NN0 ) -> ( B ^ ( -u K - 1 ) ) = ( ( B ^ -u K ) / B ) )
41 40 eqcomd 
 |-  ( ( B e. NN /\ K e. ( ZZ \ NN0 ) /\ N e. NN0 ) -> ( ( B ^ -u K ) / B ) = ( B ^ ( -u K - 1 ) ) )
42 41 oveq1d 
 |-  ( ( B e. NN /\ K e. ( ZZ \ NN0 ) /\ N e. NN0 ) -> ( ( ( B ^ -u K ) / B ) x. N ) = ( ( B ^ ( -u K - 1 ) ) x. N ) )
43 35 42 eqtrd 
 |-  ( ( B e. NN /\ K e. ( ZZ \ NN0 ) /\ N e. NN0 ) -> ( ( ( B ^ -u K ) x. N ) / B ) = ( ( B ^ ( -u K - 1 ) ) x. N ) )
44 nnm1nn0 
 |-  ( -u K e. NN -> ( -u K - 1 ) e. NN0 )
45 12 44 syl 
 |-  ( K e. ( ZZ \ NN0 ) -> ( -u K - 1 ) e. NN0 )
46 zexpcl 
 |-  ( ( B e. ZZ /\ ( -u K - 1 ) e. NN0 ) -> ( B ^ ( -u K - 1 ) ) e. ZZ )
47 9 45 46 syl2an 
 |-  ( ( B e. NN /\ K e. ( ZZ \ NN0 ) ) -> ( B ^ ( -u K - 1 ) ) e. ZZ )
48 47 3adant3 
 |-  ( ( B e. NN /\ K e. ( ZZ \ NN0 ) /\ N e. NN0 ) -> ( B ^ ( -u K - 1 ) ) e. ZZ )
49 48 18 zmulcld 
 |-  ( ( B e. NN /\ K e. ( ZZ \ NN0 ) /\ N e. NN0 ) -> ( ( B ^ ( -u K - 1 ) ) x. N ) e. ZZ )
50 43 49 eqeltrd 
 |-  ( ( B e. NN /\ K e. ( ZZ \ NN0 ) /\ N e. NN0 ) -> ( ( ( B ^ -u K ) x. N ) / B ) e. ZZ )
51 25 3adant3 
 |-  ( ( B e. NN /\ K e. ( ZZ \ NN0 ) /\ N e. NN0 ) -> ( B ^ -u K ) e. RR )
52 3 3ad2ant3 
 |-  ( ( B e. NN /\ K e. ( ZZ \ NN0 ) /\ N e. NN0 ) -> N e. RR )
53 51 52 remulcld 
 |-  ( ( B e. NN /\ K e. ( ZZ \ NN0 ) /\ N e. NN0 ) -> ( ( B ^ -u K ) x. N ) e. RR )
54 nnrp 
 |-  ( B e. NN -> B e. RR+ )
55 54 3ad2ant1 
 |-  ( ( B e. NN /\ K e. ( ZZ \ NN0 ) /\ N e. NN0 ) -> B e. RR+ )
56 mod0 
 |-  ( ( ( ( B ^ -u K ) x. N ) e. RR /\ B e. RR+ ) -> ( ( ( ( B ^ -u K ) x. N ) mod B ) = 0 <-> ( ( ( B ^ -u K ) x. N ) / B ) e. ZZ ) )
57 53 55 56 syl2anc 
 |-  ( ( B e. NN /\ K e. ( ZZ \ NN0 ) /\ N e. NN0 ) -> ( ( ( ( B ^ -u K ) x. N ) mod B ) = 0 <-> ( ( ( B ^ -u K ) x. N ) / B ) e. ZZ ) )
58 50 57 mpbird 
 |-  ( ( B e. NN /\ K e. ( ZZ \ NN0 ) /\ N e. NN0 ) -> ( ( ( B ^ -u K ) x. N ) mod B ) = 0 )
59 22 58 eqtrd 
 |-  ( ( B e. NN /\ K e. ( ZZ \ NN0 ) /\ N e. NN0 ) -> ( ( |_ ` ( ( B ^ -u K ) x. N ) ) mod B ) = 0 )
60 8 59 eqtrd 
 |-  ( ( B e. NN /\ K e. ( ZZ \ NN0 ) /\ N e. NN0 ) -> ( K ( digit ` B ) N ) = 0 )