bits0o

Description: The zeroth bit of an odd number is zero. (Contributed by Mario Carneiro, 5-Sep-2016)

		Ref	Expression
	Assertion	bits0o	$⊢ N \in ℤ \to 0 \in bits (2 \cdot N + 1)$

Step	Hyp	Ref	Expression
1		2z	$⊢ 2 \in ℤ$
2		dvdsmul1	$⊢ (2 \in ℤ \land N \in ℤ) \to 2 ∥ 2 \cdot N$
3	1 2	mpan	$⊢ N \in ℤ \to 2 ∥ 2 \cdot N$
4	1	a1i	$⊢ N \in ℤ \to 2 \in ℤ$
5		id	$⊢ N \in ℤ \to N \in ℤ$
6	4 5	zmulcld	$⊢ N \in ℤ \to 2 \cdot N \in ℤ$
7		2nn	$⊢ 2 \in ℕ$
8	7	a1i	$⊢ N \in ℤ \to 2 \in ℕ$
9		1lt2	$⊢ 1 < 2$
10	9	a1i	$⊢ N \in ℤ \to 1 < 2$
11		ndvdsp1	$⊢ (2 \cdot N \in ℤ \land 2 \in ℕ \land 1 < 2) \to (2 ∥ 2 \cdot N \to \neg 2 ∥ (2 \cdot N + 1))$
12	6 8 10 11	syl3anc	$⊢ N \in ℤ \to (2 ∥ 2 \cdot N \to \neg 2 ∥ (2 \cdot N + 1))$
13	3 12	mpd	$⊢ N \in ℤ \to \neg 2 ∥ (2 \cdot N + 1)$
14	6	peano2zd	$⊢ N \in ℤ \to 2 \cdot N + 1 \in ℤ$
15		bits0	$⊢ 2 \cdot N + 1 \in ℤ \to (0 \in bits (2 \cdot N + 1) \leftrightarrow \neg 2 ∥ (2 \cdot N + 1))$
16	14 15	syl	$⊢ N \in ℤ \to (0 \in bits (2 \cdot N + 1) \leftrightarrow \neg 2 ∥ (2 \cdot N + 1))$
17	13 16	mpbird	$⊢ N \in ℤ \to 0 \in bits (2 \cdot N + 1)$

Metamath Proof Explorer