Metamath Proof Explorer


Theorem nn0ob

Description: Alternate characterizations of an odd nonnegative integer. (Contributed by AV, 4-Jun-2020)

Ref Expression
Assertion nn0ob N0N+120N120

Proof

Step Hyp Ref Expression
1 nn0o N0N+120N120
2 nn0cn N0N
3 xp1d2m1eqxm1d2 NN+121=N12
4 3 eqcomd NN12=N+121
5 2 4 syl N0N12=N+121
6 peano2cnm NN1
7 2 6 syl N0N1
8 7 halfcld N0N12
9 1cnd N01
10 peano2nn0 N0N+10
11 10 nn0cnd N0N+1
12 11 halfcld N0N+12
13 8 9 12 addlsub N0N12+1=N+12N12=N+121
14 5 13 mpbird N0N12+1=N+12
15 14 adantr N0N120N12+1=N+12
16 peano2nn0 N120N12+10
17 16 adantl N0N120N12+10
18 15 17 eqeltrrd N0N120N+120
19 1 18 impbida N0N+120N120