Theorem 0bits

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

	Ref	Expression
Assertion	0bits	|- ( bits ` 0 ) = (/)

Proof

Step	Hyp	Ref	Expression
1		c0ex	|- 0 e. _V
2	1	snid	|- 0 e. { 0 }
3		fzo01	|- ( 0 ..^ 1 ) = { 0 }
4	2 3	eleqtrri	|- 0 e. ( 0 ..^ 1 )
5		2cn	|- 2 e. CC
6		exp0	|- ( 2 e. CC -> ( 2 ^ 0 ) = 1 )
7	5 6	ax-mp	|- ( 2 ^ 0 ) = 1
8	7	oveq2i	|- ( 0 ..^ ( 2 ^ 0 ) ) = ( 0 ..^ 1 )
9	4 8	eleqtrri	|- 0 e. ( 0 ..^ ( 2 ^ 0 ) )
10		0z	|- 0 e. ZZ
11		0nn0	|- 0 e. NN0
12		bitsfzo	|- ( ( 0 e. ZZ /\ 0 e. NN0 ) -> ( 0 e. ( 0 ..^ ( 2 ^ 0 ) ) <-> ( bits ` 0 ) C_ ( 0 ..^ 0 ) ) )
13	10 11 12	mp2an	|- ( 0 e. ( 0 ..^ ( 2 ^ 0 ) ) <-> ( bits ` 0 ) C_ ( 0 ..^ 0 ) )
14	9 13	mpbi	|- ( bits ` 0 ) C_ ( 0 ..^ 0 )
15		fzo0	|- ( 0 ..^ 0 ) = (/)
16	14 15	sseqtri	|- ( bits ` 0 ) C_ (/)
17		0ss	|- (/) C_ ( bits ` 0 )
18	16 17	eqssi	|- ( bits ` 0 ) = (/)