Metamath Proof Explorer

Theorem zeo2ALTV

Description: An integer is even or odd but not both. (Contributed by Mario Carneiro, 12-Sep-2015) (Revised by AV, 16-Jun-2020)

Ref Expression
Assertion zeo2ALTV ⊢ Z ∈ ℤ → Z ∈ Even ↔ ¬ Z ∈ Odd

Proof

Step Hyp Ref Expression
1 evennodd ⊢ Z ∈ Even → ¬ Z ∈ Odd
2 zeoALTV ⊢ Z ∈ ℤ → Z ∈ Even ∨ Z ∈ Odd
3 ax-1 ⊢ Z ∈ Even → ¬ Z ∈ Odd → Z ∈ Even
4 pm2.24 ⊢ Z ∈ Odd → ¬ Z ∈ Odd → Z ∈ Even
5 3 4 jaoi ⊢ Z ∈ Even ∨ Z ∈ Odd → ¬ Z ∈ Odd → Z ∈ Even
6 2 5 syl ⊢ Z ∈ ℤ → ¬ Z ∈ Odd → Z ∈ Even
7 1 6 impbid2 ⊢ Z ∈ ℤ → Z ∈ Even ↔ ¬ Z ∈ Odd