Metamath Proof Explorer


Theorem zob

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

Ref Expression
Assertion zob NN+12N12

Proof

Step Hyp Ref Expression
1 peano2zm N+12N+121
2 peano2z N+121N+12-1+1
3 peano2z NN+1
4 3 zcnd NN+1
5 4 halfcld NN+12
6 npcan1 N+12N+12-1+1=N+12
7 5 6 syl NN+12-1+1=N+12
8 7 eqcomd NN+12=N+12-1+1
9 8 eleq1d NN+12N+12-1+1
10 2 9 syl5ibr NN+121N+12
11 1 10 impbid2 NN+12N+121
12 zcn NN
13 xp1d2m1eqxm1d2 NN+121=N12
14 12 13 syl NN+121=N12
15 14 eleq1d NN+121N12
16 11 15 bitrd NN+12N12