Database
ELEMENTARY NUMBER THEORY
Elementary properties of divisibility
Bit sequences
bits0
Next ⟩
bits0e
Metamath Proof Explorer
Ascii
Unicode
Theorem
bits0
Description:
Value of the zeroth bit.
(Contributed by
Mario Carneiro
, 5-Sep-2016)
Ref
Expression
Assertion
bits0
⊢
N
∈
ℤ
→
0
∈
bits
⁡
N
↔
¬
2
∥
N
Proof
Step
Hyp
Ref
Expression
1
0nn0
⊢
0
∈
ℕ
0
2
bitsval2
⊢
N
∈
ℤ
∧
0
∈
ℕ
0
→
0
∈
bits
⁡
N
↔
¬
2
∥
N
2
0
3
1
2
mpan2
⊢
N
∈
ℤ
→
0
∈
bits
⁡
N
↔
¬
2
∥
N
2
0
4
2cn
⊢
2
∈
ℂ
5
exp0
⊢
2
∈
ℂ
→
2
0
=
1
6
4
5
ax-mp
⊢
2
0
=
1
7
6
oveq2i
⊢
N
2
0
=
N
1
8
zcn
⊢
N
∈
ℤ
→
N
∈
ℂ
9
8
div1d
⊢
N
∈
ℤ
→
N
1
=
N
10
7
9
syl5eq
⊢
N
∈
ℤ
→
N
2
0
=
N
11
10
fveq2d
⊢
N
∈
ℤ
→
N
2
0
=
N
12
flid
⊢
N
∈
ℤ
→
N
=
N
13
11
12
eqtrd
⊢
N
∈
ℤ
→
N
2
0
=
N
14
13
breq2d
⊢
N
∈
ℤ
→
2
∥
N
2
0
↔
2
∥
N
15
14
notbid
⊢
N
∈
ℤ
→
¬
2
∥
N
2
0
↔
¬
2
∥
N
16
3
15
bitrd
⊢
N
∈
ℤ
→
0
∈
bits
⁡
N
↔
¬
2
∥
N