Theorem n2dvds1

Description: 2 does not divide 1. That means 1 is odd. (Contributed by David A. Wheeler, 8-Dec-2018) (Proof shortened by Steven Nguyen, 3-May-2023)

	Ref	Expression
Assertion	n2dvds1	$$⊢\neg 2\parallel 1$$

Proof

Step	Hyp	Ref	Expression
1		halfnz	$$⊢\neg \frac{1}{2}\in \mathbb{Z}$$
2		1z	$$⊢1\in \mathbb{Z}$$
3		evend2	$$⊢1\in \mathbb{Z}\to \left(2\parallel 1\leftrightarrow \frac{1}{2}\in \mathbb{Z}\right)$$
4	2 3	ax-mp	$$⊢2\parallel 1\leftrightarrow \frac{1}{2}\in \mathbb{Z}$$
5	1 4	mtbir	$$⊢\neg 2\parallel 1$$