Theorem dig2nn0

Description: A digit of a nonnegative integer N in a binary system is either 0 or 1. (Contributed by AV, 24-May-2020)

	Ref	Expression
Assertion	dig2nn0	|- ( ( N e. NN0 /\ K e. ZZ ) -> ( K ( digit ` 2 ) N ) e. { 0 , 1 } )

Proof

Step	Hyp	Ref	Expression
1		2nn	|- 2 e. NN
2	1	a1i	|- ( ( N e. NN0 /\ K e. ZZ ) -> 2 e. NN )
3		simpr	|- ( ( N e. NN0 /\ K e. ZZ ) -> K e. ZZ )
4		nn0rp0	|- ( N e. NN0 -> N e. ( 0 [,) +oo ) )
5	4	adantr	|- ( ( N e. NN0 /\ K e. ZZ ) -> N e. ( 0 [,) +oo ) )
6		digval	|- ( ( 2 e. NN /\ K e. ZZ /\ N e. ( 0 [,) +oo ) ) -> ( K ( digit ` 2 ) N ) = ( ( |_ ` ( ( 2 ^ -u K ) x. N ) ) mod 2 ) )
7	2 3 5 6	syl3anc	|- ( ( N e. NN0 /\ K e. ZZ ) -> ( K ( digit ` 2 ) N ) = ( ( |_ ` ( ( 2 ^ -u K ) x. N ) ) mod 2 ) )
8		2re	|- 2 e. RR
9	8	a1i	|- ( ( N e. NN0 /\ K e. ZZ ) -> 2 e. RR )
10		2ne0	|- 2 =/= 0
11	10	a1i	|- ( ( N e. NN0 /\ K e. ZZ ) -> 2 =/= 0 )
12		znegcl	|- ( K e. ZZ -> -u K e. ZZ )
13	12	adantl	|- ( ( N e. NN0 /\ K e. ZZ ) -> -u K e. ZZ )
14	9 11 13	reexpclzd	|- ( ( N e. NN0 /\ K e. ZZ ) -> ( 2 ^ -u K ) e. RR )
15		nn0re	|- ( N e. NN0 -> N e. RR )
16	15	adantr	|- ( ( N e. NN0 /\ K e. ZZ ) -> N e. RR )
17	14 16	remulcld	|- ( ( N e. NN0 /\ K e. ZZ ) -> ( ( 2 ^ -u K ) x. N ) e. RR )
18	17	flcld	|- ( ( N e. NN0 /\ K e. ZZ ) -> ( |_ ` ( ( 2 ^ -u K ) x. N ) ) e. ZZ )
19		elmod2	|- ( ( |_ ` ( ( 2 ^ -u K ) x. N ) ) e. ZZ -> ( ( |_ ` ( ( 2 ^ -u K ) x. N ) ) mod 2 ) e. { 0 , 1 } )
20	18 19	syl	|- ( ( N e. NN0 /\ K e. ZZ ) -> ( ( |_ ` ( ( 2 ^ -u K ) x. N ) ) mod 2 ) e. { 0 , 1 } )
21	7 20	eqeltrd	|- ( ( N e. NN0 /\ K e. ZZ ) -> ( K ( digit ` 2 ) N ) e. { 0 , 1 } )