Theorem oddnn02np1

Description: A nonnegative integer is odd iff it is one plus twice another nonnegative integer. (Contributed by AV, 19-Jun-2021)

	Ref	Expression
Assertion	oddnn02np1	⊢ ( 𝑁 ∈ ℕ0 → ( ¬ 2 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℕ0 ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		eleq1	⊢ ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → ( ( ( 2 · 𝑛 ) + 1 ) ∈ ℕ0 ↔ 𝑁 ∈ ℕ0 ) )
2		elnn0z	⊢ ( ( ( 2 · 𝑛 ) + 1 ) ∈ ℕ0 ↔ ( ( ( 2 · 𝑛 ) + 1 ) ∈ ℤ ∧ 0 ≤ ( ( 2 · 𝑛 ) + 1 ) ) )
3		2tnp1ge0ge0	⊢ ( 𝑛 ∈ ℤ → ( 0 ≤ ( ( 2 · 𝑛 ) + 1 ) ↔ 0 ≤ 𝑛 ) )
4	3	biimpd	⊢ ( 𝑛 ∈ ℤ → ( 0 ≤ ( ( 2 · 𝑛 ) + 1 ) → 0 ≤ 𝑛 ) )
5	4	imdistani	⊢ ( ( 𝑛 ∈ ℤ ∧ 0 ≤ ( ( 2 · 𝑛 ) + 1 ) ) → ( 𝑛 ∈ ℤ ∧ 0 ≤ 𝑛 ) )
6	5	expcom	⊢ ( 0 ≤ ( ( 2 · 𝑛 ) + 1 ) → ( 𝑛 ∈ ℤ → ( 𝑛 ∈ ℤ ∧ 0 ≤ 𝑛 ) ) )
7		elnn0z	⊢ ( 𝑛 ∈ ℕ0 ↔ ( 𝑛 ∈ ℤ ∧ 0 ≤ 𝑛 ) )
8	6 7	imbitrrdi	⊢ ( 0 ≤ ( ( 2 · 𝑛 ) + 1 ) → ( 𝑛 ∈ ℤ → 𝑛 ∈ ℕ0 ) )
9	2 8	simplbiim	⊢ ( ( ( 2 · 𝑛 ) + 1 ) ∈ ℕ0 → ( 𝑛 ∈ ℤ → 𝑛 ∈ ℕ0 ) )
10	1 9	syl6bir	⊢ ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → ( 𝑁 ∈ ℕ0 → ( 𝑛 ∈ ℤ → 𝑛 ∈ ℕ0 ) ) )
11	10	com13	⊢ ( 𝑛 ∈ ℤ → ( 𝑁 ∈ ℕ0 → ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → 𝑛 ∈ ℕ0 ) ) )
12	11	impcom	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℤ ) → ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → 𝑛 ∈ ℕ0 ) )
13	12	pm4.71rd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℤ ) → ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ↔ ( 𝑛 ∈ ℕ0 ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) )
14	13	bicomd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℤ ) → ( ( 𝑛 ∈ ℕ0 ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ↔ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )
15	14	rexbidva	⊢ ( 𝑁 ∈ ℕ0 → ( ∃ 𝑛 ∈ ℤ ( 𝑛 ∈ ℕ0 ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ↔ ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )
16		nn0ssz	⊢ ℕ0 ⊆ ℤ
17		rexss	⊢ ( ℕ0 ⊆ ℤ → ( ∃ 𝑛 ∈ ℕ0 ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 ∈ ℕ0 ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) )
18	16 17	mp1i	⊢ ( 𝑁 ∈ ℕ0 → ( ∃ 𝑛 ∈ ℕ0 ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 ∈ ℕ0 ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) )
19		nn0z	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
20		odd2np1	⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )
21	19 20	syl	⊢ ( 𝑁 ∈ ℕ0 → ( ¬ 2 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )
22	15 18 21	3bitr4rd	⊢ ( 𝑁 ∈ ℕ0 → ( ¬ 2 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℕ0 ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )