Theorem n2dvdsm1

Description: 2 does not divide -1. That means -1 is odd. (Contributed by AV, 15-Aug-2021)

	Ref	Expression
Assertion	n2dvdsm1	$$⊢\neg 2\parallel -1$$

Proof

Step	Hyp	Ref	Expression
1		z0even	$$⊢2\parallel 0$$
2		ax-1cn	$$⊢1\in ℂ$$
3		neg1cn	$$⊢-1\in ℂ$$
4		1pneg1e0	$$⊢1+-1=0$$
5	2 3 4	addcomli	$$⊢-1+1=0$$
6	1 5	breqtrri	$$⊢2\parallel \left(-1+1\right)$$
7		neg1z	$$⊢-1\in \mathbb{Z}$$
8		oddp1even	$$⊢-1\in \mathbb{Z}\to \left(\neg 2\parallel -1\leftrightarrow 2\parallel \left(-1+1\right)\right)$$
9	7 8	ax-mp	$$⊢\neg 2\parallel -1\leftrightarrow 2\parallel \left(-1+1\right)$$
10	6 9	mpbir	$$⊢\neg 2\parallel -1$$