Metamath Proof Explorer
Description: A positive integer is even or odd but not both. (Contributed by NM, 20-Aug-2001) (Revised by AV, 19-Jun-2020)
|
|
Ref |
Expression |
|
Hypothesis |
nneoiALTV.1 |
⊢ 𝑁 ∈ ℕ |
|
Assertion |
nneoiALTV |
⊢ ( 𝑁 ∈ Even ↔ ¬ 𝑁 ∈ Odd ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
nneoiALTV.1 |
⊢ 𝑁 ∈ ℕ |
2 |
|
nneoALTV |
⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ∈ Even ↔ ¬ 𝑁 ∈ Odd ) ) |
3 |
1 2
|
ax-mp |
⊢ ( 𝑁 ∈ Even ↔ ¬ 𝑁 ∈ Odd ) |