Theorem m1bits

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

	Ref	Expression
Assertion	m1bits	⊢ ( bits ‘ - 1 ) = ℕ0

Proof

Step	Hyp	Ref	Expression
1		0z	⊢ 0 ∈ ℤ
2		bitscmp	⊢ ( 0 ∈ ℤ → ( ℕ0 ∖ ( bits ‘ 0 ) ) = ( bits ‘ ( - 0 − 1 ) ) )
3	1 2	ax-mp	⊢ ( ℕ0 ∖ ( bits ‘ 0 ) ) = ( bits ‘ ( - 0 − 1 ) )
4		0bits	⊢ ( bits ‘ 0 ) = ∅
5	4	difeq2i	⊢ ( ℕ0 ∖ ( bits ‘ 0 ) ) = ( ℕ0 ∖ ∅ )
6		dif0	⊢ ( ℕ0 ∖ ∅ ) = ℕ0
7	5 6	eqtri	⊢ ( ℕ0 ∖ ( bits ‘ 0 ) ) = ℕ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	⊢ ( bits ‘ ( - 0 − 1 ) ) = ( bits ‘ - 1 )
13	3 7 12	3eqtr3ri	⊢ ( bits ‘ - 1 ) = ℕ0