bits0

Description: Value of the zeroth bit. (Contributed by Mario Carneiro, 5-Sep-2016)

		Ref	Expression
	Assertion	bits0	$⊢ N \in ℤ \to (0 \in bits (N) \leftrightarrow \neg 2 ∥ N)$

Step	Hyp	Ref	Expression
1		0nn0	$⊢ 0 \in ℕ_{0}$
2		bitsval2	$⊢ (N \in ℤ \land 0 \in ℕ_{0}) \to (0 \in bits (N) \leftrightarrow \neg 2 ∥ ⌊\frac{N}{2^{0}}⌋)$
3	1 2	mpan2	$⊢ N \in ℤ \to (0 \in bits (N) \leftrightarrow \neg 2 ∥ ⌊\frac{N}{2^{0}}⌋)$
4		2cn	$⊢ 2 \in ℂ$
5		exp0	$⊢ 2 \in ℂ \to 2^{0} = 1$
6	4 5	ax-mp	$⊢ 2^{0} = 1$
7	6	oveq2i	$⊢ \frac{N}{2^{0}} = \frac{N}{1}$
8		zcn	$⊢ N \in ℤ \to N \in ℂ$
9	8	div1d	$⊢ N \in ℤ \to \frac{N}{1} = N$
10	7 9	eqtrid	$⊢ N \in ℤ \to \frac{N}{2^{0}} = N$
11	10	fveq2d	$⊢ N \in ℤ \to ⌊\frac{N}{2^{0}}⌋ = ⌊N⌋$
12		flid	$⊢ N \in ℤ \to ⌊N⌋ = N$
13	11 12	eqtrd	$⊢ N \in ℤ \to ⌊\frac{N}{2^{0}}⌋ = N$
14	13	breq2d	$⊢ N \in ℤ \to (2 ∥ ⌊\frac{N}{2^{0}}⌋ \leftrightarrow 2 ∥ N)$
15	14	notbid	$⊢ N \in ℤ \to (\neg 2 ∥ ⌊\frac{N}{2^{0}}⌋ \leftrightarrow \neg 2 ∥ N)$
16	3 15	bitrd	$⊢ N \in ℤ \to (0 \in bits (N) \leftrightarrow \neg 2 ∥ N)$

Metamath Proof Explorer