Theorem digvalnn0

Description: The K th digit of a nonnegative real number R in the positional system with base B is a nonnegative integer. (Contributed by AV, 28-May-2020)

	Ref	Expression
Assertion	digvalnn0	|- ( ( B e. NN /\ K e. ZZ /\ R e. ( 0 [,) +oo ) ) -> ( K ( digit ` B ) R ) e. NN0 )

Proof

Step	Hyp	Ref	Expression
1		digval	|- ( ( B e. NN /\ K e. ZZ /\ R e. ( 0 [,) +oo ) ) -> ( K ( digit ` B ) R ) = ( ( |_ ` ( ( B ^ -u K ) x. R ) ) mod B ) )
2		nnre	|- ( B e. NN -> B e. RR )
3	2	3ad2ant1	|- ( ( B e. NN /\ K e. ZZ /\ R e. ( 0 [,) +oo ) ) -> B e. RR )
4		nnne0	|- ( B e. NN -> B =/= 0 )
5	4	3ad2ant1	|- ( ( B e. NN /\ K e. ZZ /\ R e. ( 0 [,) +oo ) ) -> B =/= 0 )
6		znegcl	|- ( K e. ZZ -> -u K e. ZZ )
7	6	3ad2ant2	|- ( ( B e. NN /\ K e. ZZ /\ R e. ( 0 [,) +oo ) ) -> -u K e. ZZ )
8	3 5 7	reexpclzd	|- ( ( B e. NN /\ K e. ZZ /\ R e. ( 0 [,) +oo ) ) -> ( B ^ -u K ) e. RR )
9		elrege0	|- ( R e. ( 0 [,) +oo ) <-> ( R e. RR /\ 0 <_ R ) )
10	9	simplbi	|- ( R e. ( 0 [,) +oo ) -> R e. RR )
11	10	3ad2ant3	|- ( ( B e. NN /\ K e. ZZ /\ R e. ( 0 [,) +oo ) ) -> R e. RR )
12	8 11	remulcld	|- ( ( B e. NN /\ K e. ZZ /\ R e. ( 0 [,) +oo ) ) -> ( ( B ^ -u K ) x. R ) e. RR )
13	12	flcld	|- ( ( B e. NN /\ K e. ZZ /\ R e. ( 0 [,) +oo ) ) -> ( |_ ` ( ( B ^ -u K ) x. R ) ) e. ZZ )
14		simp1	|- ( ( B e. NN /\ K e. ZZ /\ R e. ( 0 [,) +oo ) ) -> B e. NN )
15	13 14	zmodcld	|- ( ( B e. NN /\ K e. ZZ /\ R e. ( 0 [,) +oo ) ) -> ( ( |_ ` ( ( B ^ -u K ) x. R ) ) mod B ) e. NN0 )
16	1 15	eqeltrd	|- ( ( B e. NN /\ K e. ZZ /\ R e. ( 0 [,) +oo ) ) -> ( K ( digit ` B ) R ) e. NN0 )