Theorem halfnz

Description: One-half is not an integer. (Contributed by NM, 31-Jul-2004)

	Ref	Expression
Assertion	halfnz	$$⊢\neg \frac{1}{2}\in \mathbb{Z}$$

Proof

Step	Hyp	Ref	Expression
1		2re	$$⊢2\in ℝ$$
2		1lt2	$$⊢1<2$$
3		recnz	$$⊢\left(2\in ℝ\wedge 1<2\right)\to \neg \frac{1}{2}\in \mathbb{Z}$$
4	1 2 3	mp2an	$$⊢\neg \frac{1}{2}\in \mathbb{Z}$$