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 ( 𝑁 ∈ { 0 , 1 } → ( 0 ( digit ‘ 2 ) 𝑁 ) = 𝑁 )

Proof

Step Hyp Ref Expression
1 elpri ⊢ ( 𝑁 ∈ { 0 , 1 } → ( 𝑁 = 0 ∨ 𝑁 = 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 ⊢ ( 𝑁 = 0 → ( 0 ( digit ‘ 2 ) 𝑁 ) = ( 0 ( digit ‘ 2 ) 0 ) )
7 id ⊢ ( 𝑁 = 0 → 𝑁 = 0 )
8 5 6 7 3eqtr4a ⊢ ( 𝑁 = 0 → ( 0 ( digit ‘ 2 ) 𝑁 ) = 𝑁 )
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 ⊢ ( 𝑁 = 1 → ( 0 ( digit ‘ 2 ) 𝑁 ) = ( 0 ( digit ‘ 2 ) 1 ) )
14 id ⊢ ( 𝑁 = 1 → 𝑁 = 1 )
15 12 13 14 3eqtr4a ⊢ ( 𝑁 = 1 → ( 0 ( digit ‘ 2 ) 𝑁 ) = 𝑁 )
16 8 15 jaoi ⊢ ( ( 𝑁 = 0 ∨ 𝑁 = 1 ) → ( 0 ( digit ‘ 2 ) 𝑁 ) = 𝑁 )
17 1 16 syl ⊢ ( 𝑁 ∈ { 0 , 1 } → ( 0 ( digit ‘ 2 ) 𝑁 ) = 𝑁 )