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