Theorem 0bits

Description: The bits of zero. (Contributed by Mario Carneiro, 6-Sep-2016)

	Ref	Expression
Assertion	0bits	$$⊢\mathrm{bits}\left(0\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		c0ex	$$⊢0\in \mathrm{V}$$
2	1	snid	$$⊢0\in \left\{0\right\}$$
3		fzo01	$$⊢\left(0..^1\right)=\left\{0\right\}$$
4	2 3	eleqtrri	$$⊢0\in \left(0..^1\right)$$
5		2cn	$$⊢2\in ℂ$$
6		exp0	$$⊢2\in ℂ\to 2^0=1$$
7	5 6	ax-mp	$$⊢2^0=1$$
8	7	oveq2i	$$⊢\left(0..^2^0\right)=\left(0..^1\right)$$
9	4 8	eleqtrri	$$⊢0\in \left(0..^2^0\right)$$
10		0z	$$⊢0\in \mathbb{Z}$$
11		0nn0	$$⊢0\in {\mathbb{N}}_0$$
12		bitsfzo	$$⊢\left(0\in \mathbb{Z}\wedge 0\in {\mathbb{N}}_0\right)\to \left(0\in \left(0..^2^0\right)\leftrightarrow \mathrm{bits}\left(0\right)\subseteq \left(0..^0\right)\right)$$
13	10 11 12	mp2an	$$⊢0\in \left(0..^2^0\right)\leftrightarrow \mathrm{bits}\left(0\right)\subseteq \left(0..^0\right)$$
14	9 13	mpbi	$$⊢\mathrm{bits}\left(0\right)\subseteq \left(0..^0\right)$$
15		fzo0	$$⊢\left(0..^0\right)=\varnothing$$
16	14 15	sseqtri	$$⊢\mathrm{bits}\left(0\right)\subseteq \varnothing$$
17		0ss	$$⊢\varnothing \subseteq \mathrm{bits}\left(0\right)$$
18	16 17	eqssi	$$⊢\mathrm{bits}\left(0\right)=\varnothing$$