Metamath Proof Explorer


Theorem nn0onn0exALTV

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) (Revised by AV, 22-Jun-2020)

Ref Expression
Assertion nn0onn0exALTV ( ( 𝑁 ∈ ℕ0𝑁 ∈ Odd ) → ∃ 𝑚 ∈ ℕ0 𝑁 = ( ( 2 · 𝑚 ) + 1 ) )

Proof

Step Hyp Ref Expression
1 nn0oALTV ( ( 𝑁 ∈ ℕ0𝑁 ∈ Odd ) → ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 )
2 simpr ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 ) → ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 )
3 oveq2 ( 𝑚 = ( ( 𝑁 − 1 ) / 2 ) → ( 2 · 𝑚 ) = ( 2 · ( ( 𝑁 − 1 ) / 2 ) ) )
4 3 oveq1d ( 𝑚 = ( ( 𝑁 − 1 ) / 2 ) → ( ( 2 · 𝑚 ) + 1 ) = ( ( 2 · ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) )
5 4 eqeq2d ( 𝑚 = ( ( 𝑁 − 1 ) / 2 ) → ( 𝑁 = ( ( 2 · 𝑚 ) + 1 ) ↔ 𝑁 = ( ( 2 · ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) ) )
6 5 adantl ( ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 ) ∧ 𝑚 = ( ( 𝑁 − 1 ) / 2 ) ) → ( 𝑁 = ( ( 2 · 𝑚 ) + 1 ) ↔ 𝑁 = ( ( 2 · ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) ) )
7 nn0cn ( 𝑁 ∈ ℕ0𝑁 ∈ ℂ )
8 peano2cnm ( 𝑁 ∈ ℂ → ( 𝑁 − 1 ) ∈ ℂ )
9 7 8 syl ( 𝑁 ∈ ℕ0 → ( 𝑁 − 1 ) ∈ ℂ )
10 2cnd ( 𝑁 ∈ ℕ0 → 2 ∈ ℂ )
11 2ne0 2 ≠ 0
12 11 a1i ( 𝑁 ∈ ℕ0 → 2 ≠ 0 )
13 9 10 12 divcan2d ( 𝑁 ∈ ℕ0 → ( 2 · ( ( 𝑁 − 1 ) / 2 ) ) = ( 𝑁 − 1 ) )
14 13 oveq1d ( 𝑁 ∈ ℕ0 → ( ( 2 · ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) = ( ( 𝑁 − 1 ) + 1 ) )
15 npcan1 ( 𝑁 ∈ ℂ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
16 7 15 syl ( 𝑁 ∈ ℕ0 → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
17 14 16 eqtr2d ( 𝑁 ∈ ℕ0𝑁 = ( ( 2 · ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) )
18 17 adantr ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 ) → 𝑁 = ( ( 2 · ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) )
19 2 6 18 rspcedvd ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 ) → ∃ 𝑚 ∈ ℕ0 𝑁 = ( ( 2 · 𝑚 ) + 1 ) )
20 1 19 syldan ( ( 𝑁 ∈ ℕ0𝑁 ∈ Odd ) → ∃ 𝑚 ∈ ℕ0 𝑁 = ( ( 2 · 𝑚 ) + 1 ) )