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	⊢ ¬ 2 ∥ 1

Proof

Step	Hyp	Ref	Expression
1		halfnz	⊢ ¬ ( 1 / 2 ) ∈ ℤ
2		1z	⊢ 1 ∈ ℤ
3		evend2	⊢ ( 1 ∈ ℤ → ( 2 ∥ 1 ↔ ( 1 / 2 ) ∈ ℤ ) )
4	2 3	ax-mp	⊢ ( 2 ∥ 1 ↔ ( 1 / 2 ) ∈ ℤ )
5	1 4	mtbir	⊢ ¬ 2 ∥ 1