bitsuz

Description: The bits of a number are all at least N iff the number is divisible by 2 ^ N . (Contributed by Mario Carneiro, 21-Sep-2016)

		Ref	Expression
	Assertion	bitsuz	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to (2^{N} ∥ A \leftrightarrow bits (A) \subseteq ℤ_{\geq N})$

Proof

Step	Hyp	Ref	Expression
1		bitsres	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to bits (A) \cap ℤ_{\geq N} = bits (⌊\frac{A}{2^{N}}⌋ 2^{N})$
2	1	eqeq1d	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to (bits (A) \cap ℤ_{\geq N} = bits (A) \leftrightarrow bits (⌊\frac{A}{2^{N}}⌋ 2^{N}) = bits (A))$
3		simpl	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to A \in ℤ$
4	3	zred	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to A \in ℝ$
5		2nn	$⊢ 2 \in ℕ$
6	5	a1i	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to 2 \in ℕ$
7		simpr	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to N \in ℕ_{0}$
8	6 7	nnexpcld	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to 2^{N} \in ℕ$
9	4 8	nndivred	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to \frac{A}{2^{N}} \in ℝ$
10	9	flcld	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to ⌊\frac{A}{2^{N}}⌋ \in ℤ$
11	8	nnzd	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to 2^{N} \in ℤ$
12	10 11	zmulcld	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to ⌊\frac{A}{2^{N}}⌋ 2^{N} \in ℤ$
13		bitsf1	$⊢ bits : ℤ \underset{1-1}{⟶} 𝒫 ℕ_{0}$
14		f1fveq	$⊢ (bits : ℤ \underset{1-1}{⟶} 𝒫 ℕ_{0} \land (⌊\frac{A}{2^{N}}⌋ 2^{N} \in ℤ \land A \in ℤ)) \to (bits (⌊\frac{A}{2^{N}}⌋ 2^{N}) = bits (A) \leftrightarrow ⌊\frac{A}{2^{N}}⌋ 2^{N} = A)$
15	13 14	mpan	$⊢ (⌊\frac{A}{2^{N}}⌋ 2^{N} \in ℤ \land A \in ℤ) \to (bits (⌊\frac{A}{2^{N}}⌋ 2^{N}) = bits (A) \leftrightarrow ⌊\frac{A}{2^{N}}⌋ 2^{N} = A)$
16	12 3 15	syl2anc	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to (bits (⌊\frac{A}{2^{N}}⌋ 2^{N}) = bits (A) \leftrightarrow ⌊\frac{A}{2^{N}}⌋ 2^{N} = A)$
17		dvdsmul2	$⊢ (⌊\frac{A}{2^{N}}⌋ \in ℤ \land 2^{N} \in ℤ) \to 2^{N} ∥ ⌊\frac{A}{2^{N}}⌋ 2^{N}$
18	10 11 17	syl2anc	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to 2^{N} ∥ ⌊\frac{A}{2^{N}}⌋ 2^{N}$
19		breq2	$⊢ ⌊\frac{A}{2^{N}}⌋ 2^{N} = A \to (2^{N} ∥ ⌊\frac{A}{2^{N}}⌋ 2^{N} \leftrightarrow 2^{N} ∥ A)$
20	18 19	syl5ibcom	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to (⌊\frac{A}{2^{N}}⌋ 2^{N} = A \to 2^{N} ∥ A)$
21	8	nnne0d	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to 2^{N} \neq 0$
22		dvdsval2	$⊢ (2^{N} \in ℤ \land 2^{N} \neq 0 \land A \in ℤ) \to (2^{N} ∥ A \leftrightarrow \frac{A}{2^{N}} \in ℤ)$
23	11 21 3 22	syl3anc	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to (2^{N} ∥ A \leftrightarrow \frac{A}{2^{N}} \in ℤ)$
24	23	biimpa	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land 2^{N} ∥ A) \to \frac{A}{2^{N}} \in ℤ$
25		flid	$⊢ \frac{A}{2^{N}} \in ℤ \to ⌊\frac{A}{2^{N}}⌋ = \frac{A}{2^{N}}$
26	24 25	syl	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land 2^{N} ∥ A) \to ⌊\frac{A}{2^{N}}⌋ = \frac{A}{2^{N}}$
27	26	oveq1d	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land 2^{N} ∥ A) \to ⌊\frac{A}{2^{N}}⌋ 2^{N} = (\frac{A}{2^{N}}) 2^{N}$
28	3	zcnd	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to A \in ℂ$
29	28	adantr	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land 2^{N} ∥ A) \to A \in ℂ$
30	8	nncnd	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to 2^{N} \in ℂ$
31	30	adantr	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land 2^{N} ∥ A) \to 2^{N} \in ℂ$
32		2cnd	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land 2^{N} ∥ A) \to 2 \in ℂ$
33		2ne0	$⊢ 2 \neq 0$
34	33	a1i	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land 2^{N} ∥ A) \to 2 \neq 0$
35	7	nn0zd	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to N \in ℤ$
36	35	adantr	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land 2^{N} ∥ A) \to N \in ℤ$
37	32 34 36	expne0d	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land 2^{N} ∥ A) \to 2^{N} \neq 0$
38	29 31 37	divcan1d	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land 2^{N} ∥ A) \to (\frac{A}{2^{N}}) 2^{N} = A$
39	27 38	eqtrd	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land 2^{N} ∥ A) \to ⌊\frac{A}{2^{N}}⌋ 2^{N} = A$
40	39	ex	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to (2^{N} ∥ A \to ⌊\frac{A}{2^{N}}⌋ 2^{N} = A)$
41	20 40	impbid	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to (⌊\frac{A}{2^{N}}⌋ 2^{N} = A \leftrightarrow 2^{N} ∥ A)$
42	2 16 41	3bitrrd	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to (2^{N} ∥ A \leftrightarrow bits (A) \cap ℤ_{\geq N} = bits (A))$
43		df-ss	$⊢ bits (A) \subseteq ℤ_{\geq N} \leftrightarrow bits (A) \cap ℤ_{\geq N} = bits (A)$
44	42 43	bitr4di	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to (2^{N} ∥ A \leftrightarrow bits (A) \subseteq ℤ_{\geq N})$

Metamath Proof Explorer

Theorem bitsuz

Proof