Theorem bits0

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

	Ref	Expression
Assertion	bits0	$$⊢N\in \mathbb{Z}\to \left(0\in \mathrm{bits}\left(N\right)\leftrightarrow \neg 2\parallel N\right)$$

Proof

Step	Hyp	Ref	Expression
1		0nn0	$$⊢0\in {\mathbb{N}}_0$$
2		bitsval2	$$⊢\left(N\in \mathbb{Z}\wedge 0\in {\mathbb{N}}_0\right)\to \left(0\in \mathrm{bits}\left(N\right)\leftrightarrow \neg 2\parallel ⌊\frac{N}{2^0}⌋\right)$$
3	1 2	mpan2	$$⊢N\in \mathbb{Z}\to \left(0\in \mathrm{bits}\left(N\right)\leftrightarrow \neg 2\parallel ⌊\frac{N}{2^0}⌋\right)$$
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 \mathbb{Z}\to N\in ℂ$$
9	8	div1d	$$⊢N\in \mathbb{Z}\to \frac{N}{1}=N$$
10	7 9	eqtrid	$$⊢N\in \mathbb{Z}\to \frac{N}{2^0}=N$$
11	10	fveq2d	$$⊢N\in \mathbb{Z}\to ⌊\frac{N}{2^0}⌋=⌊N⌋$$
12		flid	$$⊢N\in \mathbb{Z}\to ⌊N⌋=N$$
13	11 12	eqtrd	$$⊢N\in \mathbb{Z}\to ⌊\frac{N}{2^0}⌋=N$$
14	13	breq2d	$$⊢N\in \mathbb{Z}\to \left(2\parallel ⌊\frac{N}{2^0}⌋\leftrightarrow 2\parallel N\right)$$
15	14	notbid	$$⊢N\in \mathbb{Z}\to \left(\neg 2\parallel ⌊\frac{N}{2^0}⌋\leftrightarrow \neg 2\parallel N\right)$$
16	3 15	bitrd	$$⊢N\in \mathbb{Z}\to \left(0\in \mathrm{bits}\left(N\right)\leftrightarrow \neg 2\parallel N\right)$$