Metamath Proof Explorer


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 ) )