Description: A positive integer is even or odd but not both. (Contributed by NM, 20-Aug-2001)
Ref | Expression | ||
---|---|---|---|
Hypothesis | nneoi.1 | |- N e. NN |
|
Assertion | nneoi | |- ( ( N / 2 ) e. NN <-> -. ( ( N + 1 ) / 2 ) e. NN ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nneoi.1 | |- N e. NN |
|
2 | nneo | |- ( N e. NN -> ( ( N / 2 ) e. NN <-> -. ( ( N + 1 ) / 2 ) e. NN ) ) |
|
3 | 1 2 | ax-mp | |- ( ( N / 2 ) e. NN <-> -. ( ( N + 1 ) / 2 ) e. NN ) |