Theorem halfnz

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

	Ref	Expression
Assertion	halfnz	|- -. ( 1 / 2 ) e. ZZ

Proof

Step	Hyp	Ref	Expression
1		2re	|- 2 e. RR
2		1lt2	|- 1 < 2
3		recnz	|- ( ( 2 e. RR /\ 1 < 2 ) -> -. ( 1 / 2 ) e. ZZ )
4	1 2 3	mp2an	|- -. ( 1 / 2 ) e. ZZ