Theorem bits0ALTV

Description: Value of the zeroth bit. (Contributed by Mario Carneiro, 5-Sep-2016) (Revised by AV, 19-Jun-2020)

	Ref	Expression
Assertion	bits0ALTV	⊢ ( 𝑁 ∈ ℤ → ( 0 ∈ ( bits ‘ 𝑁 ) ↔ 𝑁 ∈ Odd ) )

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		isodd3	⊢ ( 𝑁 ∈ Odd ↔ ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) )
17	16	baibr	⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 ↔ 𝑁 ∈ Odd ) )
18	3 15 17	3bitrd	⊢ ( 𝑁 ∈ ℤ → ( 0 ∈ ( bits ‘ 𝑁 ) ↔ 𝑁 ∈ Odd ) )