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 ∈ V
2	1	snid	⊢ 0 ∈ { 0 }
3		fzo01	⊢ ( 0 ..^ 1 ) = { 0 }
4	2 3	eleqtrri	⊢ 0 ∈ ( 0 ..^ 1 )
5		2cn	⊢ 2 ∈ ℂ
6		exp0	⊢ ( 2 ∈ ℂ → ( 2 ↑ 0 ) = 1 )
7	5 6	ax-mp	⊢ ( 2 ↑ 0 ) = 1
8	7	oveq2i	⊢ ( 0 ..^ ( 2 ↑ 0 ) ) = ( 0 ..^ 1 )
9	4 8	eleqtrri	⊢ 0 ∈ ( 0 ..^ ( 2 ↑ 0 ) )
10		0z	⊢ 0 ∈ ℤ
11		0nn0	⊢ 0 ∈ ℕ0
12		bitsfzo	⊢ ( ( 0 ∈ ℤ ∧ 0 ∈ ℕ0 ) → ( 0 ∈ ( 0 ..^ ( 2 ↑ 0 ) ) ↔ ( bits ‘ 0 ) ⊆ ( 0 ..^ 0 ) ) )
13	10 11 12	mp2an	⊢ ( 0 ∈ ( 0 ..^ ( 2 ↑ 0 ) ) ↔ ( bits ‘ 0 ) ⊆ ( 0 ..^ 0 ) )
14	9 13	mpbi	⊢ ( bits ‘ 0 ) ⊆ ( 0 ..^ 0 )
15		fzo0	⊢ ( 0 ..^ 0 ) = ∅
16	14 15	sseqtri	⊢ ( bits ‘ 0 ) ⊆ ∅
17		0ss	⊢ ∅ ⊆ ( bits ‘ 0 )
18	16 17	eqssi	⊢ ( bits ‘ 0 ) = ∅