bits0ALTV

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

		Ref	Expression
	Assertion	bits0ALTV	$⊢ N \in ℤ \to (0 \in bits (N) \leftrightarrow N \in Odd)$

Step	Hyp	Ref	Expression
1		0nn0	$⊢ 0 \in ℕ_{0}$
2		bitsval2	$⊢ (N \in ℤ \land 0 \in ℕ_{0}) \to (0 \in bits (N) \leftrightarrow \neg 2 ∥ ⌊\frac{N}{2^{0}}⌋)$
3	1 2	mpan2	$⊢ N \in ℤ \to (0 \in bits (N) \leftrightarrow \neg 2 ∥ ⌊\frac{N}{2^{0}}⌋)$
4		2cn	$⊢ 2 \in ℂ$
5		exp0	$⊢ 2 \in ℂ \to 2^{0} = 1$
6	4 5	ax-mp	$⊢ 2^{0} = 1$
7	6	oveq2i	$⊢ \frac{N}{2^{0}} = \frac{N}{1}$
8		zcn	$⊢ N \in ℤ \to N \in ℂ$
9	8	div1d	$⊢ N \in ℤ \to \frac{N}{1} = N$
10	7 9	eqtrid	$⊢ N \in ℤ \to \frac{N}{2^{0}} = N$
11	10	fveq2d	$⊢ N \in ℤ \to ⌊\frac{N}{2^{0}}⌋ = ⌊N⌋$
12		flid	$⊢ N \in ℤ \to ⌊N⌋ = N$
13	11 12	eqtrd	$⊢ N \in ℤ \to ⌊\frac{N}{2^{0}}⌋ = N$
14	13	breq2d	$⊢ N \in ℤ \to (2 ∥ ⌊\frac{N}{2^{0}}⌋ \leftrightarrow 2 ∥ N)$
15	14	notbid	$⊢ N \in ℤ \to (\neg 2 ∥ ⌊\frac{N}{2^{0}}⌋ \leftrightarrow \neg 2 ∥ N)$
16		isodd3	$⊢ N \in Odd \leftrightarrow (N \in ℤ \land \neg 2 ∥ N)$
17	16	baibr	$⊢ N \in ℤ \to (\neg 2 ∥ N \leftrightarrow N \in Odd)$
18	3 15 17	3bitrd	$⊢ N \in ℤ \to (0 \in bits (N) \leftrightarrow N \in Odd)$

Metamath Proof Explorer