Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Complexity theory
Digits
0dig2pr01
Next ⟩
dig2nn0
Metamath Proof Explorer
Ascii
Unicode
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