Theorem halfnz

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

	Ref	Expression
Assertion	halfnz	⊢ ¬ ( 1 / 2 ) ∈ ℤ

Proof

Step	Hyp	Ref	Expression
1		2re	⊢ 2 ∈ ℝ
2		1lt2	⊢ 1 < 2
3		recnz	⊢ ( ( 2 ∈ ℝ ∧ 1 < 2 ) → ¬ ( 1 / 2 ) ∈ ℤ )
4	1 2 3	mp2an	⊢ ¬ ( 1 / 2 ) ∈ ℤ