Theorem bits0

Description: Value of the zeroth bit. (Contributed by Mario Carneiro, 5-Sep-2016)

	Ref	Expression
Assertion	bits0	⊢ ( 𝑁 ∈ ℤ → ( 0 ∈ ( bits ‘ 𝑁 ) ↔ ¬ 2 ∥ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		0nn0	⊢ 0 ∈ ℕ0
2		bitsval2	⊢ ( ( 𝑁 ∈ ℤ ∧ 0 ∈ ℕ0 ) → ( 0 ∈ ( bits ‘ 𝑁 ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 0 ) ) ) ) )
3	1 2	mpan2	⊢ ( 𝑁 ∈ ℤ → ( 0 ∈ ( bits ‘ 𝑁 ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 0 ) ) ) ) )
4		2cn	⊢ 2 ∈ ℂ
5		exp0	⊢ ( 2 ∈ ℂ → ( 2 ↑ 0 ) = 1 )
6	4 5	ax-mp	⊢ ( 2 ↑ 0 ) = 1
7	6	oveq2i	⊢ ( 𝑁 / ( 2 ↑ 0 ) ) = ( 𝑁 / 1 )
8		zcn	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
9	8	div1d	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 / 1 ) = 𝑁 )
10	7 9	syl5eq	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 / ( 2 ↑ 0 ) ) = 𝑁 )
11	10	fveq2d	⊢ ( 𝑁 ∈ ℤ → ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 0 ) ) ) = ( ⌊ ‘ 𝑁 ) )
12		flid	⊢ ( 𝑁 ∈ ℤ → ( ⌊ ‘ 𝑁 ) = 𝑁 )
13	11 12	eqtrd	⊢ ( 𝑁 ∈ ℤ → ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 0 ) ) ) = 𝑁 )
14	13	breq2d	⊢ ( 𝑁 ∈ ℤ → ( 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 0 ) ) ) ↔ 2 ∥ 𝑁 ) )
15	14	notbid	⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 0 ) ) ) ↔ ¬ 2 ∥ 𝑁 ) )
16	3 15	bitrd	⊢ ( 𝑁 ∈ ℤ → ( 0 ∈ ( bits ‘ 𝑁 ) ↔ ¬ 2 ∥ 𝑁 ) )