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	⊢ ( 𝑍 ∈ ℤ → ( 𝑍 ∈ Even ↔ ¬ 𝑍 ∈ Odd ) )

Proof

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