# Metamath Proof Explorer

## Theorem oddnn02np1

Description: A nonnegative integer is odd iff it is one plus twice another nonnegative integer. (Contributed by AV, 19-Jun-2021)

Ref Expression
Assertion oddnn02np1 ${⊢}{N}\in {ℕ}_{0}\to \left(¬2\parallel {N}↔\exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}2{n}+1={N}\right)$

### Proof

Step Hyp Ref Expression
1 eleq1 ${⊢}2{n}+1={N}\to \left(2{n}+1\in {ℕ}_{0}↔{N}\in {ℕ}_{0}\right)$
2 elnn0z ${⊢}2{n}+1\in {ℕ}_{0}↔\left(2{n}+1\in ℤ\wedge 0\le 2{n}+1\right)$
3 2tnp1ge0ge0 ${⊢}{n}\in ℤ\to \left(0\le 2{n}+1↔0\le {n}\right)$
4 3 biimpd ${⊢}{n}\in ℤ\to \left(0\le 2{n}+1\to 0\le {n}\right)$
5 4 imdistani ${⊢}\left({n}\in ℤ\wedge 0\le 2{n}+1\right)\to \left({n}\in ℤ\wedge 0\le {n}\right)$
6 5 expcom ${⊢}0\le 2{n}+1\to \left({n}\in ℤ\to \left({n}\in ℤ\wedge 0\le {n}\right)\right)$
7 elnn0z ${⊢}{n}\in {ℕ}_{0}↔\left({n}\in ℤ\wedge 0\le {n}\right)$
8 6 7 syl6ibr ${⊢}0\le 2{n}+1\to \left({n}\in ℤ\to {n}\in {ℕ}_{0}\right)$
9 2 8 simplbiim ${⊢}2{n}+1\in {ℕ}_{0}\to \left({n}\in ℤ\to {n}\in {ℕ}_{0}\right)$
10 1 9 syl6bir ${⊢}2{n}+1={N}\to \left({N}\in {ℕ}_{0}\to \left({n}\in ℤ\to {n}\in {ℕ}_{0}\right)\right)$
11 10 com13 ${⊢}{n}\in ℤ\to \left({N}\in {ℕ}_{0}\to \left(2{n}+1={N}\to {n}\in {ℕ}_{0}\right)\right)$
12 11 impcom ${⊢}\left({N}\in {ℕ}_{0}\wedge {n}\in ℤ\right)\to \left(2{n}+1={N}\to {n}\in {ℕ}_{0}\right)$
13 12 pm4.71rd ${⊢}\left({N}\in {ℕ}_{0}\wedge {n}\in ℤ\right)\to \left(2{n}+1={N}↔\left({n}\in {ℕ}_{0}\wedge 2{n}+1={N}\right)\right)$
14 13 bicomd ${⊢}\left({N}\in {ℕ}_{0}\wedge {n}\in ℤ\right)\to \left(\left({n}\in {ℕ}_{0}\wedge 2{n}+1={N}\right)↔2{n}+1={N}\right)$
15 14 rexbidva ${⊢}{N}\in {ℕ}_{0}\to \left(\exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}\left({n}\in {ℕ}_{0}\wedge 2{n}+1={N}\right)↔\exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}2{n}+1={N}\right)$
16 nn0ssz ${⊢}{ℕ}_{0}\subseteq ℤ$
17 rexss ${⊢}{ℕ}_{0}\subseteq ℤ\to \left(\exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}2{n}+1={N}↔\exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}\left({n}\in {ℕ}_{0}\wedge 2{n}+1={N}\right)\right)$
18 16 17 mp1i ${⊢}{N}\in {ℕ}_{0}\to \left(\exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}2{n}+1={N}↔\exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}\left({n}\in {ℕ}_{0}\wedge 2{n}+1={N}\right)\right)$
19 nn0z ${⊢}{N}\in {ℕ}_{0}\to {N}\in ℤ$
20 odd2np1 ${⊢}{N}\in ℤ\to \left(¬2\parallel {N}↔\exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}2{n}+1={N}\right)$
21 19 20 syl ${⊢}{N}\in {ℕ}_{0}\to \left(¬2\parallel {N}↔\exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}2{n}+1={N}\right)$
22 15 18 21 3bitr4rd ${⊢}{N}\in {ℕ}_{0}\to \left(¬2\parallel {N}↔\exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}2{n}+1={N}\right)$