Theorem n2dvdsm1

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

	Ref	Expression
Assertion	n2dvdsm1	⊢ ¬ 2 ∥ - 1

Proof

Step	Hyp	Ref	Expression
1		z0even	⊢ 2 ∥ 0
2		ax-1cn	⊢ 1 ∈ ℂ
3		neg1cn	⊢ - 1 ∈ ℂ
4		1pneg1e0	⊢ ( 1 + - 1 ) = 0
5	2 3 4	addcomli	⊢ ( - 1 + 1 ) = 0
6	1 5	breqtrri	⊢ 2 ∥ ( - 1 + 1 )
7		neg1z	⊢ - 1 ∈ ℤ
8		oddp1even	⊢ ( - 1 ∈ ℤ → ( ¬ 2 ∥ - 1 ↔ 2 ∥ ( - 1 + 1 ) ) )
9	7 8	ax-mp	⊢ ( ¬ 2 ∥ - 1 ↔ 2 ∥ ( - 1 + 1 ) )
10	6 9	mpbir	⊢ ¬ 2 ∥ - 1