This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )