# Metamath Proof Explorer

## 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 ${⊢}\left({N}\in {ℕ}_{0}\wedge {K}\in ℤ\right)\to {K}\mathrm{digit}\left(2\right){N}\in \left\{0,1\right\}$

### Proof

Step Hyp Ref Expression
1 2nn ${⊢}2\in ℕ$
2 1 a1i ${⊢}\left({N}\in {ℕ}_{0}\wedge {K}\in ℤ\right)\to 2\in ℕ$
3 simpr ${⊢}\left({N}\in {ℕ}_{0}\wedge {K}\in ℤ\right)\to {K}\in ℤ$
4 nn0rp0 ${⊢}{N}\in {ℕ}_{0}\to {N}\in \left[0,\mathrm{+\infty }\right)$
5 4 adantr ${⊢}\left({N}\in {ℕ}_{0}\wedge {K}\in ℤ\right)\to {N}\in \left[0,\mathrm{+\infty }\right)$
6 digval ${⊢}\left(2\in ℕ\wedge {K}\in ℤ\wedge {N}\in \left[0,\mathrm{+\infty }\right)\right)\to {K}\mathrm{digit}\left(2\right){N}=⌊{2}^{-{K}}\cdot {N}⌋\mathrm{mod}2$
7 2 3 5 6 syl3anc ${⊢}\left({N}\in {ℕ}_{0}\wedge {K}\in ℤ\right)\to {K}\mathrm{digit}\left(2\right){N}=⌊{2}^{-{K}}\cdot {N}⌋\mathrm{mod}2$
8 2re ${⊢}2\in ℝ$
9 8 a1i ${⊢}\left({N}\in {ℕ}_{0}\wedge {K}\in ℤ\right)\to 2\in ℝ$
10 2ne0 ${⊢}2\ne 0$
11 10 a1i ${⊢}\left({N}\in {ℕ}_{0}\wedge {K}\in ℤ\right)\to 2\ne 0$
12 znegcl ${⊢}{K}\in ℤ\to -{K}\in ℤ$
13 12 adantl ${⊢}\left({N}\in {ℕ}_{0}\wedge {K}\in ℤ\right)\to -{K}\in ℤ$
14 9 11 13 reexpclzd ${⊢}\left({N}\in {ℕ}_{0}\wedge {K}\in ℤ\right)\to {2}^{-{K}}\in ℝ$
15 nn0re ${⊢}{N}\in {ℕ}_{0}\to {N}\in ℝ$
16 15 adantr ${⊢}\left({N}\in {ℕ}_{0}\wedge {K}\in ℤ\right)\to {N}\in ℝ$
17 14 16 remulcld ${⊢}\left({N}\in {ℕ}_{0}\wedge {K}\in ℤ\right)\to {2}^{-{K}}\cdot {N}\in ℝ$
18 17 flcld ${⊢}\left({N}\in {ℕ}_{0}\wedge {K}\in ℤ\right)\to ⌊{2}^{-{K}}\cdot {N}⌋\in ℤ$
19 elmod2 ${⊢}⌊{2}^{-{K}}\cdot {N}⌋\in ℤ\to ⌊{2}^{-{K}}\cdot {N}⌋\mathrm{mod}2\in \left\{0,1\right\}$
20 18 19 syl ${⊢}\left({N}\in {ℕ}_{0}\wedge {K}\in ℤ\right)\to ⌊{2}^{-{K}}\cdot {N}⌋\mathrm{mod}2\in \left\{0,1\right\}$
21 7 20 eqeltrd ${⊢}\left({N}\in {ℕ}_{0}\wedge {K}\in ℤ\right)\to {K}\mathrm{digit}\left(2\right){N}\in \left\{0,1\right\}$