Theorem dig2bits

Description: The K th digit of a nonnegative integer N in a binary system is its K th bit. (Contributed by AV, 24-May-2020)

	Ref	Expression
Assertion	dig2bits	$$⊢\left(N\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\right)\to \left(K\mathrm{digit}\left(2\right)N=1\leftrightarrow K\in \mathrm{bits}\left(N\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		nn0re	$$⊢N\in {\mathbb{N}}_0\to N\in ℝ$$
2	1	adantr	$$⊢\left(N\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\right)\to N\in ℝ$$
3		2re	$$⊢2\in ℝ$$
4	3	a1i	$$⊢N\in {\mathbb{N}}_0\to 2\in ℝ$$
5		reexpcl	$$⊢\left(2\in ℝ\wedge K\in {\mathbb{N}}_0\right)\to 2^K\in ℝ$$
6	4 5	sylan	$$⊢\left(N\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\right)\to 2^K\in ℝ$$
7		2cnd	$$⊢\left(N\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\right)\to 2\in ℂ$$
8		2ne0	$$⊢2\ne 0$$
9	8	a1i	$$⊢\left(N\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\right)\to 2\ne 0$$
10		nn0z	$$⊢K\in {\mathbb{N}}_0\to K\in \mathbb{Z}$$
11	10	adantl	$$⊢\left(N\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\right)\to K\in \mathbb{Z}$$
12	7 9 11	expne0d	$$⊢\left(N\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\right)\to 2^K\ne 0$$
13	2 6 12	redivcld	$$⊢\left(N\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\right)\to \frac{N}{2^K}\in ℝ$$
14	13	flcld	$$⊢\left(N\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\right)\to ⌊\frac{N}{2^K}⌋\in \mathbb{Z}$$
15		mod2eq1n2dvds	$$⊢⌊\frac{N}{2^K}⌋\in \mathbb{Z}\to \left(⌊\frac{N}{2^K}⌋\mathrm{mod}2=1\leftrightarrow \neg 2\parallel ⌊\frac{N}{2^K}⌋\right)$$
16	14 15	syl	$$⊢\left(N\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\right)\to \left(⌊\frac{N}{2^K}⌋\mathrm{mod}2=1\leftrightarrow \neg 2\parallel ⌊\frac{N}{2^K}⌋\right)$$
17		2nn	$$⊢2\in \mathbb{N}$$
18	17	a1i	$$⊢\left(N\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\right)\to 2\in \mathbb{N}$$
19		simpr	$$⊢\left(N\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\right)\to K\in {\mathbb{N}}_0$$
20		nn0rp0	$$⊢N\in {\mathbb{N}}_0\to N\in \left[0,\mathrm{+\infty }\right)$$
21	20	adantr	$$⊢\left(N\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\right)\to N\in \left[0,\mathrm{+\infty }\right)$$
22		nn0digval	$$⊢\left(2\in \mathbb{N}\wedge K\in {\mathbb{N}}_0\wedge N\in \left[0,\mathrm{+\infty }\right)\right)\to K\mathrm{digit}\left(2\right)N=⌊\frac{N}{2^K}⌋\mathrm{mod}2$$
23	18 19 21 22	syl3anc	$$⊢\left(N\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\right)\to K\mathrm{digit}\left(2\right)N=⌊\frac{N}{2^K}⌋\mathrm{mod}2$$
24	23	eqeq1d	$$⊢\left(N\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\right)\to \left(K\mathrm{digit}\left(2\right)N=1\leftrightarrow ⌊\frac{N}{2^K}⌋\mathrm{mod}2=1\right)$$
25		nn0z	$$⊢N\in {\mathbb{N}}_0\to N\in \mathbb{Z}$$
26		bitsval2	$$⊢\left(N\in \mathbb{Z}\wedge K\in {\mathbb{N}}_0\right)\to \left(K\in \mathrm{bits}\left(N\right)\leftrightarrow \neg 2\parallel ⌊\frac{N}{2^K}⌋\right)$$
27	25 26	sylan	$$⊢\left(N\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\right)\to \left(K\in \mathrm{bits}\left(N\right)\leftrightarrow \neg 2\parallel ⌊\frac{N}{2^K}⌋\right)$$
28	16 24 27	3bitr4d	$$⊢\left(N\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\right)\to \left(K\mathrm{digit}\left(2\right)N=1\leftrightarrow K\in \mathrm{bits}\left(N\right)\right)$$