Theorem zeo2

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

	Ref	Expression
Assertion	zeo2	⊢ ( 𝑁 ∈ ℤ → ( ( 𝑁 / 2 ) ∈ ℤ ↔ ¬ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )

Proof

Step	Hyp	Ref	Expression
1		zcn	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
2		peano2cn	⊢ ( 𝑁 ∈ ℂ → ( 𝑁 + 1 ) ∈ ℂ )
3	1 2	syl	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 + 1 ) ∈ ℂ )
4		2cnd	⊢ ( 𝑁 ∈ ℤ → 2 ∈ ℂ )
5		2ne0	⊢ 2 ≠ 0
6	5	a1i	⊢ ( 𝑁 ∈ ℤ → 2 ≠ 0 )
7	3 4 6	divcan2d	⊢ ( 𝑁 ∈ ℤ → ( 2 · ( ( 𝑁 + 1 ) / 2 ) ) = ( 𝑁 + 1 ) )
8	1 4 6	divcan2d	⊢ ( 𝑁 ∈ ℤ → ( 2 · ( 𝑁 / 2 ) ) = 𝑁 )
9	8	oveq1d	⊢ ( 𝑁 ∈ ℤ → ( ( 2 · ( 𝑁 / 2 ) ) + 1 ) = ( 𝑁 + 1 ) )
10	7 9	eqtr4d	⊢ ( 𝑁 ∈ ℤ → ( 2 · ( ( 𝑁 + 1 ) / 2 ) ) = ( ( 2 · ( 𝑁 / 2 ) ) + 1 ) )
11		zneo	⊢ ( ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ∧ ( 𝑁 / 2 ) ∈ ℤ ) → ( 2 · ( ( 𝑁 + 1 ) / 2 ) ) ≠ ( ( 2 · ( 𝑁 / 2 ) ) + 1 ) )
12	11	expcom	⊢ ( ( 𝑁 / 2 ) ∈ ℤ → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ → ( 2 · ( ( 𝑁 + 1 ) / 2 ) ) ≠ ( ( 2 · ( 𝑁 / 2 ) ) + 1 ) ) )
13	12	necon2bd	⊢ ( ( 𝑁 / 2 ) ∈ ℤ → ( ( 2 · ( ( 𝑁 + 1 ) / 2 ) ) = ( ( 2 · ( 𝑁 / 2 ) ) + 1 ) → ¬ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )
14	10 13	syl5com	⊢ ( 𝑁 ∈ ℤ → ( ( 𝑁 / 2 ) ∈ ℤ → ¬ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )
15		zeo	⊢ ( 𝑁 ∈ ℤ → ( ( 𝑁 / 2 ) ∈ ℤ ∨ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )
16	15	ord	⊢ ( 𝑁 ∈ ℤ → ( ¬ ( 𝑁 / 2 ) ∈ ℤ → ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )
17	16	con1d	⊢ ( 𝑁 ∈ ℤ → ( ¬ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ → ( 𝑁 / 2 ) ∈ ℤ ) )
18	14 17	impbid	⊢ ( 𝑁 ∈ ℤ → ( ( 𝑁 / 2 ) ∈ ℤ ↔ ¬ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )