Theorem nn0ob

Description: Alternate characterizations of an odd nonnegative integer. (Contributed by AV, 4-Jun-2020)

	Ref	Expression
Assertion	nn0ob	⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ↔ ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 ) )

Proof

Step	Hyp	Ref	Expression
1		nn0o	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 )
2		nn0cn	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
3		xp1d2m1eqxm1d2	⊢ ( 𝑁 ∈ ℂ → ( ( ( 𝑁 + 1 ) / 2 ) − 1 ) = ( ( 𝑁 − 1 ) / 2 ) )
4	3	eqcomd	⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 − 1 ) / 2 ) = ( ( ( 𝑁 + 1 ) / 2 ) − 1 ) )
5	2 4	syl	⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 − 1 ) / 2 ) = ( ( ( 𝑁 + 1 ) / 2 ) − 1 ) )
6		peano2cnm	⊢ ( 𝑁 ∈ ℂ → ( 𝑁 − 1 ) ∈ ℂ )
7	2 6	syl	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 − 1 ) ∈ ℂ )
8	7	halfcld	⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 − 1 ) / 2 ) ∈ ℂ )
9		1cnd	⊢ ( 𝑁 ∈ ℕ0 → 1 ∈ ℂ )
10		peano2nn0	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
11	10	nn0cnd	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℂ )
12	11	halfcld	⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) / 2 ) ∈ ℂ )
13	8 9 12	addlsub	⊢ ( 𝑁 ∈ ℕ0 → ( ( ( ( 𝑁 − 1 ) / 2 ) + 1 ) = ( ( 𝑁 + 1 ) / 2 ) ↔ ( ( 𝑁 − 1 ) / 2 ) = ( ( ( 𝑁 + 1 ) / 2 ) − 1 ) ) )
14	5 13	mpbird	⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 𝑁 − 1 ) / 2 ) + 1 ) = ( ( 𝑁 + 1 ) / 2 ) )
15	14	adantr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 ) → ( ( ( 𝑁 − 1 ) / 2 ) + 1 ) = ( ( 𝑁 + 1 ) / 2 ) )
16		peano2nn0	⊢ ( ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 → ( ( ( 𝑁 − 1 ) / 2 ) + 1 ) ∈ ℕ0 )
17	16	adantl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 ) → ( ( ( 𝑁 − 1 ) / 2 ) + 1 ) ∈ ℕ0 )
18	15 17	eqeltrrd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 ) → ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 )
19	1 18	impbida	⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ↔ ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 ) )