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 ⊢ N ∈ ℕ 0 ∧ N + 1 2 ∈ ℕ 0 → ∃ m ∈ ℕ 0 N = 2 ⁢ m + 1

Proof

Step Hyp Ref Expression
1 nn0o ⊢ N ∈ ℕ 0 ∧ N + 1 2 ∈ ℕ 0 → N − 1 2 ∈ ℕ 0
2 simpr ⊢ N ∈ ℕ 0 ∧ N − 1 2 ∈ ℕ 0 → N − 1 2 ∈ ℕ 0
3 oveq2 ⊢ m = N − 1 2 → 2 ⁢ m = 2 ⁢ N − 1 2
4 3 oveq1d ⊢ m = N − 1 2 → 2 ⁢ m + 1 = 2 ⁢ N − 1 2 + 1
5 4 eqeq2d ⊢ m = N − 1 2 → N = 2 ⁢ m + 1 ↔ N = 2 ⁢ N − 1 2 + 1
6 5 adantl ⊢ N ∈ ℕ 0 ∧ N − 1 2 ∈ ℕ 0 ∧ m = N − 1 2 → N = 2 ⁢ m + 1 ↔ N = 2 ⁢ N − 1 2 + 1
7 nn0cn ⊢ N ∈ ℕ 0 → N ∈ ℂ
8 peano2cnm ⊢ N ∈ ℂ → N − 1 ∈ ℂ
9 7 8 syl ⊢ N ∈ ℕ 0 → N − 1 ∈ ℂ
10 2cnd ⊢ N ∈ ℕ 0 → 2 ∈ ℂ
11 2ne0 ⊢ 2 ≠ 0
12 11 a1i ⊢ N ∈ ℕ 0 → 2 ≠ 0
13 9 10 12 divcan2d ⊢ N ∈ ℕ 0 → 2 ⁢ N − 1 2 = N − 1
14 13 oveq1d ⊢ N ∈ ℕ 0 → 2 ⁢ N − 1 2 + 1 = N - 1 + 1
15 npcan1 ⊢ N ∈ ℂ → N - 1 + 1 = N
16 7 15 syl ⊢ N ∈ ℕ 0 → N - 1 + 1 = N
17 14 16 eqtr2d ⊢ N ∈ ℕ 0 → N = 2 ⁢ N − 1 2 + 1
18 17 adantr ⊢ N ∈ ℕ 0 ∧ N − 1 2 ∈ ℕ 0 → N = 2 ⁢ N − 1 2 + 1
19 2 6 18 rspcedvd ⊢ N ∈ ℕ 0 ∧ N − 1 2 ∈ ℕ 0 → ∃ m ∈ ℕ 0 N = 2 ⁢ m + 1
20 1 19 syldan ⊢ N ∈ ℕ 0 ∧ N + 1 2 ∈ ℕ 0 → ∃ m ∈ ℕ 0 N = 2 ⁢ m + 1