Theorem 1odd

Description: 1 is an odd integer. (Contributed by AV, 3-Feb-2020)

	Ref	Expression
Hypothesis	oddinmgm.e	⊢ 𝑂 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 2 · 𝑥 ) + 1 ) }
Assertion	1odd	⊢ 1 ∈ 𝑂

Proof

Step	Hyp	Ref	Expression
1		oddinmgm.e	⊢ 𝑂 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 2 · 𝑥 ) + 1 ) }
2		1z	⊢ 1 ∈ ℤ
3		0z	⊢ 0 ∈ ℤ
4		id	⊢ ( 0 ∈ ℤ → 0 ∈ ℤ )
5		oveq2	⊢ ( 𝑥 = 0 → ( 2 · 𝑥 ) = ( 2 · 0 ) )
6		2t0e0	⊢ ( 2 · 0 ) = 0
7	5 6	eqtrdi	⊢ ( 𝑥 = 0 → ( 2 · 𝑥 ) = 0 )
8	7	oveq1d	⊢ ( 𝑥 = 0 → ( ( 2 · 𝑥 ) + 1 ) = ( 0 + 1 ) )
9	8	eqeq2d	⊢ ( 𝑥 = 0 → ( 1 = ( ( 2 · 𝑥 ) + 1 ) ↔ 1 = ( 0 + 1 ) ) )
10	9	adantl	⊢ ( ( 0 ∈ ℤ ∧ 𝑥 = 0 ) → ( 1 = ( ( 2 · 𝑥 ) + 1 ) ↔ 1 = ( 0 + 1 ) ) )
11		1e0p1	⊢ 1 = ( 0 + 1 )
12	11	a1i	⊢ ( 0 ∈ ℤ → 1 = ( 0 + 1 ) )
13	4 10 12	rspcedvd	⊢ ( 0 ∈ ℤ → ∃ 𝑥 ∈ ℤ 1 = ( ( 2 · 𝑥 ) + 1 ) )
14	3 13	ax-mp	⊢ ∃ 𝑥 ∈ ℤ 1 = ( ( 2 · 𝑥 ) + 1 )
15		eqeq1	⊢ ( 𝑧 = 1 → ( 𝑧 = ( ( 2 · 𝑥 ) + 1 ) ↔ 1 = ( ( 2 · 𝑥 ) + 1 ) ) )
16	15	rexbidv	⊢ ( 𝑧 = 1 → ( ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 2 · 𝑥 ) + 1 ) ↔ ∃ 𝑥 ∈ ℤ 1 = ( ( 2 · 𝑥 ) + 1 ) ) )
17	16 1	elrab2	⊢ ( 1 ∈ 𝑂 ↔ ( 1 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 1 = ( ( 2 · 𝑥 ) + 1 ) ) )
18	2 14 17	mpbir2an	⊢ 1 ∈ 𝑂