bits0e

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

		Ref	Expression
	Assertion	bits0e	$⊢ N \in ℤ \to \neg 0 \in bits (2 \cdot N)$

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		bits0	$⊢ 2 \cdot N \in ℤ \to (0 \in bits (2 \cdot N) \leftrightarrow \neg 2 ∥ 2 \cdot N)$
8	6 7	syl	$⊢ N \in ℤ \to (0 \in bits (2 \cdot N) \leftrightarrow \neg 2 ∥ 2 \cdot N)$
9	8	con2bid	$⊢ N \in ℤ \to (2 ∥ 2 \cdot N \leftrightarrow \neg 0 \in bits (2 \cdot N))$
10	3 9	mpbid	$⊢ N \in ℤ \to \neg 0 \in bits (2 \cdot N)$

Metamath Proof Explorer