This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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