Metamath Proof Explorer


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