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 \in ℕ_{0} \land K \in ℤ) \to K digit (2) N \in \{0, 1\}$

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

Metamath Proof Explorer