Metamath Proof Explorer

Theorem 0dig2pr01

Description: The integers 0 and 1 correspond to their last bit. (Contributed by AV, 28-May-2010)

Ref Expression
Assertion 0dig2pr01 
|- ( N e. { 0 , 1 } -> ( 0 ( digit ` 2 ) N ) = N )

Proof

Step Hyp Ref Expression
1 elpri 
 |-  ( N e. { 0 , 1 } -> ( N = 0 \/ N = 1 ) )
2 2nn 
 |-  2 e. NN
3 0z 
 |-  0 e. ZZ
4 dig0 
 |-  ( ( 2 e. NN /\ 0 e. ZZ ) -> ( 0 ( digit ` 2 ) 0 ) = 0 )
5 2 3 4 mp2an 
 |-  ( 0 ( digit ` 2 ) 0 ) = 0
6 oveq2 
 |-  ( N = 0 -> ( 0 ( digit ` 2 ) N ) = ( 0 ( digit ` 2 ) 0 ) )
7 id 
 |-  ( N = 0 -> N = 0 )
8 5 6 7 3eqtr4a 
 |-  ( N = 0 -> ( 0 ( digit ` 2 ) N ) = N )
9 2z 
 |-  2 e. ZZ
10 uzid 
 |-  ( 2 e. ZZ -> 2 e. ( ZZ>= ` 2 ) )
11 0dig1 
 |-  ( 2 e. ( ZZ>= ` 2 ) -> ( 0 ( digit ` 2 ) 1 ) = 1 )
12 9 10 11 mp2b 
 |-  ( 0 ( digit ` 2 ) 1 ) = 1
13 oveq2 
 |-  ( N = 1 -> ( 0 ( digit ` 2 ) N ) = ( 0 ( digit ` 2 ) 1 ) )
14 id 
 |-  ( N = 1 -> N = 1 )
15 12 13 14 3eqtr4a 
 |-  ( N = 1 -> ( 0 ( digit ` 2 ) N ) = N )
16 8 15 jaoi 
 |-  ( ( N = 0 \/ N = 1 ) -> ( 0 ( digit ` 2 ) N ) = N )
17 1 16 syl 
 |-  ( N e. { 0 , 1 } -> ( 0 ( digit ` 2 ) N ) = N )