Theorem m1bits

Description: The bits of negative one. (Contributed by Mario Carneiro, 5-Sep-2016)

	Ref	Expression
Assertion	m1bits	$$⊢\mathrm{bits}\left(-1\right)={\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		0z	$$⊢0\in \mathbb{Z}$$
2		bitscmp	$$⊢0\in \mathbb{Z}\to {\mathbb{N}}_0\setminus \mathrm{bits}\left(0\right)=\mathrm{bits}\left(-0-1\right)$$
3	1 2	ax-mp	$$⊢{\mathbb{N}}_0\setminus \mathrm{bits}\left(0\right)=\mathrm{bits}\left(-0-1\right)$$
4		0bits	$$⊢\mathrm{bits}\left(0\right)=\varnothing$$
5	4	difeq2i	$$⊢{\mathbb{N}}_0\setminus \mathrm{bits}\left(0\right)={\mathbb{N}}_0\setminus \varnothing$$
6		dif0	$$⊢{\mathbb{N}}_0\setminus \varnothing ={\mathbb{N}}_0$$
7	5 6	eqtri	$$⊢{\mathbb{N}}_0\setminus \mathrm{bits}\left(0\right)={\mathbb{N}}_0$$
8		neg0	$$⊢-0=0$$
9	8	oveq1i	$$⊢-0-1=0-1$$
10		df-neg	$$⊢-1=0-1$$
11	9 10	eqtr4i	$$⊢-0-1=-1$$
12	11	fveq2i	$$⊢\mathrm{bits}\left(-0-1\right)=\mathrm{bits}\left(-1\right)$$
13	3 7 12	3eqtr3ri	$$⊢\mathrm{bits}\left(-1\right)={\mathbb{N}}_0$$