Theorem zob

Description: Alternate characterizations of an odd number. (Contributed by AV, 7-Jun-2020)

	Ref	Expression
Assertion	zob	⊢ ( 𝑁 ∈ ℤ → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ↔ ( ( 𝑁 − 1 ) / 2 ) ∈ ℤ ) )

Proof

Step	Hyp	Ref	Expression
1		peano2zm	⊢ ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ → ( ( ( 𝑁 + 1 ) / 2 ) − 1 ) ∈ ℤ )
2		peano2z	⊢ ( ( ( ( 𝑁 + 1 ) / 2 ) − 1 ) ∈ ℤ → ( ( ( ( 𝑁 + 1 ) / 2 ) − 1 ) + 1 ) ∈ ℤ )
3		peano2z	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 + 1 ) ∈ ℤ )
4	3	zcnd	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 + 1 ) ∈ ℂ )
5	4	halfcld	⊢ ( 𝑁 ∈ ℤ → ( ( 𝑁 + 1 ) / 2 ) ∈ ℂ )
6		npcan1	⊢ ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℂ → ( ( ( ( 𝑁 + 1 ) / 2 ) − 1 ) + 1 ) = ( ( 𝑁 + 1 ) / 2 ) )
7	5 6	syl	⊢ ( 𝑁 ∈ ℤ → ( ( ( ( 𝑁 + 1 ) / 2 ) − 1 ) + 1 ) = ( ( 𝑁 + 1 ) / 2 ) )
8	7	eqcomd	⊢ ( 𝑁 ∈ ℤ → ( ( 𝑁 + 1 ) / 2 ) = ( ( ( ( 𝑁 + 1 ) / 2 ) − 1 ) + 1 ) )
9	8	eleq1d	⊢ ( 𝑁 ∈ ℤ → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ↔ ( ( ( ( 𝑁 + 1 ) / 2 ) − 1 ) + 1 ) ∈ ℤ ) )
10	2 9	syl5ibr	⊢ ( 𝑁 ∈ ℤ → ( ( ( ( 𝑁 + 1 ) / 2 ) − 1 ) ∈ ℤ → ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )
11	1 10	impbid2	⊢ ( 𝑁 ∈ ℤ → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ↔ ( ( ( 𝑁 + 1 ) / 2 ) − 1 ) ∈ ℤ ) )
12		zcn	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
13		xp1d2m1eqxm1d2	⊢ ( 𝑁 ∈ ℂ → ( ( ( 𝑁 + 1 ) / 2 ) − 1 ) = ( ( 𝑁 − 1 ) / 2 ) )
14	12 13	syl	⊢ ( 𝑁 ∈ ℤ → ( ( ( 𝑁 + 1 ) / 2 ) − 1 ) = ( ( 𝑁 − 1 ) / 2 ) )
15	14	eleq1d	⊢ ( 𝑁 ∈ ℤ → ( ( ( ( 𝑁 + 1 ) / 2 ) − 1 ) ∈ ℤ ↔ ( ( 𝑁 − 1 ) / 2 ) ∈ ℤ ) )
16	11 15	bitrd	⊢ ( 𝑁 ∈ ℤ → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ↔ ( ( 𝑁 − 1 ) / 2 ) ∈ ℤ ) )