Theorem odd2np1ALTV

Description: An integer is odd iff it is one plus twice another integer. (Contributed by Scott Fenton, 3-Apr-2014) (Revised by AV, 19-Jun-2020)

	Ref	Expression
Assertion	odd2np1ALTV	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 ∈ Odd ↔ ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		ibar	⊢ ( 𝑁 ∈ ℤ → ( ∃ 𝑛 ∈ ℤ 𝑁 = ( ( 2 · 𝑛 ) + 1 ) ↔ ( 𝑁 ∈ ℤ ∧ ∃ 𝑛 ∈ ℤ 𝑁 = ( ( 2 · 𝑛 ) + 1 ) ) ) )
2		eqcom	⊢ ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ↔ 𝑁 = ( ( 2 · 𝑛 ) + 1 ) )
3	2	a1i	⊢ ( 𝑁 ∈ ℤ → ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ↔ 𝑁 = ( ( 2 · 𝑛 ) + 1 ) ) )
4	3	rexbidv	⊢ ( 𝑁 ∈ ℤ → ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ↔ ∃ 𝑛 ∈ ℤ 𝑁 = ( ( 2 · 𝑛 ) + 1 ) ) )
5		eqeq1	⊢ ( 𝑧 = 𝑁 → ( 𝑧 = ( ( 2 · 𝑛 ) + 1 ) ↔ 𝑁 = ( ( 2 · 𝑛 ) + 1 ) ) )
6	5	rexbidv	⊢ ( 𝑧 = 𝑁 → ( ∃ 𝑛 ∈ ℤ 𝑧 = ( ( 2 · 𝑛 ) + 1 ) ↔ ∃ 𝑛 ∈ ℤ 𝑁 = ( ( 2 · 𝑛 ) + 1 ) ) )
7		dfodd6	⊢ Odd = { 𝑧 ∈ ℤ ∣ ∃ 𝑛 ∈ ℤ 𝑧 = ( ( 2 · 𝑛 ) + 1 ) }
8	6 7	elrab2	⊢ ( 𝑁 ∈ Odd ↔ ( 𝑁 ∈ ℤ ∧ ∃ 𝑛 ∈ ℤ 𝑁 = ( ( 2 · 𝑛 ) + 1 ) ) )
9	8	a1i	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 ∈ Odd ↔ ( 𝑁 ∈ ℤ ∧ ∃ 𝑛 ∈ ℤ 𝑁 = ( ( 2 · 𝑛 ) + 1 ) ) ) )
10	1 4 9	3bitr4rd	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 ∈ Odd ↔ ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )