Metamath Proof Explorer

Theorem nn0onn0ex

Description: For each odd nonnegative integer there is a nonnegative integer which, multiplied by 2 and increased by 1, results in the odd nonnegative integer. (Contributed by AV, 30-May-2020)

Ref Expression
Assertion nn0onn0ex ${⊢}\left({N}\in {ℕ}_{0}\wedge \frac{{N}+1}{2}\in {ℕ}_{0}\right)\to \exists {m}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{N}=2{m}+1$

Proof

Step Hyp Ref Expression
1 nn0o ${⊢}\left({N}\in {ℕ}_{0}\wedge \frac{{N}+1}{2}\in {ℕ}_{0}\right)\to \frac{{N}-1}{2}\in {ℕ}_{0}$
2 simpr ${⊢}\left({N}\in {ℕ}_{0}\wedge \frac{{N}-1}{2}\in {ℕ}_{0}\right)\to \frac{{N}-1}{2}\in {ℕ}_{0}$
3 oveq2 ${⊢}{m}=\frac{{N}-1}{2}\to 2{m}=2\left(\frac{{N}-1}{2}\right)$
4 3 oveq1d ${⊢}{m}=\frac{{N}-1}{2}\to 2{m}+1=2\left(\frac{{N}-1}{2}\right)+1$
5 4 eqeq2d ${⊢}{m}=\frac{{N}-1}{2}\to \left({N}=2{m}+1↔{N}=2\left(\frac{{N}-1}{2}\right)+1\right)$
6 5 adantl ${⊢}\left(\left({N}\in {ℕ}_{0}\wedge \frac{{N}-1}{2}\in {ℕ}_{0}\right)\wedge {m}=\frac{{N}-1}{2}\right)\to \left({N}=2{m}+1↔{N}=2\left(\frac{{N}-1}{2}\right)+1\right)$
7 nn0cn ${⊢}{N}\in {ℕ}_{0}\to {N}\in ℂ$
8 peano2cnm ${⊢}{N}\in ℂ\to {N}-1\in ℂ$
9 7 8 syl ${⊢}{N}\in {ℕ}_{0}\to {N}-1\in ℂ$
10 2cnd ${⊢}{N}\in {ℕ}_{0}\to 2\in ℂ$
11 2ne0 ${⊢}2\ne 0$
12 11 a1i ${⊢}{N}\in {ℕ}_{0}\to 2\ne 0$
13 9 10 12 divcan2d ${⊢}{N}\in {ℕ}_{0}\to 2\left(\frac{{N}-1}{2}\right)={N}-1$
14 13 oveq1d ${⊢}{N}\in {ℕ}_{0}\to 2\left(\frac{{N}-1}{2}\right)+1={N}-1+1$
15 npcan1 ${⊢}{N}\in ℂ\to {N}-1+1={N}$
16 7 15 syl ${⊢}{N}\in {ℕ}_{0}\to {N}-1+1={N}$
17 14 16 eqtr2d ${⊢}{N}\in {ℕ}_{0}\to {N}=2\left(\frac{{N}-1}{2}\right)+1$
18 17 adantr ${⊢}\left({N}\in {ℕ}_{0}\wedge \frac{{N}-1}{2}\in {ℕ}_{0}\right)\to {N}=2\left(\frac{{N}-1}{2}\right)+1$
19 2 6 18 rspcedvd ${⊢}\left({N}\in {ℕ}_{0}\wedge \frac{{N}-1}{2}\in {ℕ}_{0}\right)\to \exists {m}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{N}=2{m}+1$
20 1 19 syldan ${⊢}\left({N}\in {ℕ}_{0}\wedge \frac{{N}+1}{2}\in {ℕ}_{0}\right)\to \exists {m}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{N}=2{m}+1$