Metamath Proof Explorer

Theorem zob

Description: Alternate characterizations of an odd number. (Contributed by AV, 7-Jun-2020)

Ref Expression
Assertion zob ⊢ N ∈ ℤ → N + 1 2 ∈ ℤ ↔ N − 1 2 ∈ ℤ

Proof

Step Hyp Ref Expression
1 peano2zm ⊢ N + 1 2 ∈ ℤ → N + 1 2 − 1 ∈ ℤ
2 peano2z ⊢ N + 1 2 − 1 ∈ ℤ → N + 1 2 - 1 + 1 ∈ ℤ
3 peano2z ⊢ N ∈ ℤ → N + 1 ∈ ℤ
4 3 zcnd ⊢ N ∈ ℤ → N + 1 ∈ ℂ
5 4 halfcld ⊢ N ∈ ℤ → N + 1 2 ∈ ℂ
6 npcan1 ⊢ N + 1 2 ∈ ℂ → N + 1 2 - 1 + 1 = N + 1 2
7 5 6 syl ⊢ N ∈ ℤ → N + 1 2 - 1 + 1 = N + 1 2
8 7 eqcomd ⊢ N ∈ ℤ → N + 1 2 = N + 1 2 - 1 + 1
9 8 eleq1d ⊢ N ∈ ℤ → N + 1 2 ∈ ℤ ↔ N + 1 2 - 1 + 1 ∈ ℤ
10 2 9 imbitrrid ⊢ N ∈ ℤ → N + 1 2 − 1 ∈ ℤ → N + 1 2 ∈ ℤ
11 1 10 impbid2 ⊢ N ∈ ℤ → N + 1 2 ∈ ℤ ↔ N + 1 2 − 1 ∈ ℤ
12 zcn ⊢ N ∈ ℤ → N ∈ ℂ
13 xp1d2m1eqxm1d2 ⊢ N ∈ ℂ → N + 1 2 − 1 = N − 1 2
14 12 13 syl ⊢ N ∈ ℤ → N + 1 2 − 1 = N − 1 2
15 14 eleq1d ⊢ N ∈ ℤ → N + 1 2 − 1 ∈ ℤ ↔ N − 1 2 ∈ ℤ
16 11 15 bitrd ⊢ N ∈ ℤ → N + 1 2 ∈ ℤ ↔ N − 1 2 ∈ ℤ