Metamath Proof Explorer

Theorem bits0eALTV

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

		Ref	Expression
	Assertion	bits0eALTV	$⊢ N \in Even \to \neg 0 \in bits (N)$

Step	Hyp	Ref	Expression
1		evennodd	$⊢ N \in Even \to \neg N \in Odd$
2		evenz	$⊢ N \in Even \to N \in ℤ$
3		bits0ALTV	$⊢ N \in ℤ \to (0 \in bits (N) \leftrightarrow N \in Odd)$
4	2 3	syl	$⊢ N \in Even \to (0 \in bits (N) \leftrightarrow N \in Odd)$
5	1 4	mtbird	$⊢ N \in Even \to \neg 0 \in bits (N)$