Metamath Proof Explorer


Theorem nn0o

Description: An alternate characterization of an odd nonnegative integer. (Contributed by AV, 28-May-2020) (Proof shortened by AV, 2-Jun-2020)

Ref Expression
Assertion nn0o N0N+120N120

Proof

Step Hyp Ref Expression
1 nn0o1gt2 N0N+120N=12<N
2 1m1e0 11=0
3 2 oveq1i 112=02
4 2cn 2
5 2ne0 20
6 4 5 div0i 02=0
7 3 6 eqtri 112=0
8 0nn0 00
9 7 8 eqeltri 1120
10 oveq1 N=1N1=11
11 10 oveq1d N=1N12=112
12 11 eleq1d N=1N1201120
13 12 adantr N=1N0N+120N1201120
14 9 13 mpbiri N=1N0N+120N120
15 14 ex N=1N0N+120N120
16 2z 2
17 16 a1i 2<NN0N+1202
18 nn0z N0N
19 18 ad2antrl 2<NN0N+120N
20 2re 2
21 nn0re N0N
22 ltle 2N2<N2N
23 20 21 22 sylancr N02<N2N
24 23 adantr N0N+1202<N2N
25 24 impcom 2<NN0N+1202N
26 eluz2 N22N2N
27 17 19 25 26 syl3anbrc 2<NN0N+120N2
28 simprr 2<NN0N+120N+120
29 27 28 jca 2<NN0N+120N2N+120
30 nno N2N+120N12
31 nnnn0 N12N120
32 29 30 31 3syl 2<NN0N+120N120
33 32 ex 2<NN0N+120N120
34 15 33 jaoi N=12<NN0N+120N120
35 1 34 mpcom N0N+120N120