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

Metamath Proof Explorer

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 imbitrrid ⊢ ( 𝑁 ∈ ℤ → ( ( ( ( 𝑁 + 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 ) ∈ ℤ ) )