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