Metamath Proof Explorer

Theorem m1bits

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

Ref Expression
Assertion m1bits 
|- ( bits ` -u 1 ) = NN0

Proof

Step Hyp Ref Expression
1 0z 
 |-  0 e. ZZ
2 bitscmp 
 |-  ( 0 e. ZZ -> ( NN0 \ ( bits ` 0 ) ) = ( bits ` ( -u 0 - 1 ) ) )
3 1 2 ax-mp 
 |-  ( NN0 \ ( bits ` 0 ) ) = ( bits ` ( -u 0 - 1 ) )
4 0bits 
 |-  ( bits ` 0 ) = (/)
5 4 difeq2i 
 |-  ( NN0 \ ( bits ` 0 ) ) = ( NN0 \ (/) )
6 dif0 
 |-  ( NN0 \ (/) ) = NN0
7 5 6 eqtri 
 |-  ( NN0 \ ( bits ` 0 ) ) = NN0
8 neg0 
 |-  -u 0 = 0
9 8 oveq1i 
 |-  ( -u 0 - 1 ) = ( 0 - 1 )
10 df-neg 
 |-  -u 1 = ( 0 - 1 )
11 9 10 eqtr4i 
 |-  ( -u 0 - 1 ) = -u 1
12 11 fveq2i 
 |-  ( bits ` ( -u 0 - 1 ) ) = ( bits ` -u 1 )
13 3 7 12 3eqtr3ri 
 |-  ( bits ` -u 1 ) = NN0