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	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ∃ 𝑚 ∈ ℕ0 𝑁 = ( ( 2 · 𝑚 ) + 1 ) )

Proof

Step	Hyp	Ref	Expression
1		nn0o	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( ( 𝑁 − 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 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ∃ 𝑚 ∈ ℕ0 𝑁 = ( ( 2 · 𝑚 ) + 1 ) )