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 0 1 0 digit 2 N = N

Proof

Step Hyp Ref Expression
1 elpri N 0 1 N = 0 N = 1
2 2nn 2
3 0z 0
4 dig0 2 0 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
10 uzid 2 2 2
11 0dig1 2 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 0 1 0 digit 2 N = N