Theorem 2nodd

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

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

Proof

Step	Hyp	Ref	Expression
1		oddinmgm.e	⊢ 𝑂 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 2 · 𝑥 ) + 1 ) }
2		halfnz	⊢ ¬ ( 1 / 2 ) ∈ ℤ
3		eleq1	⊢ ( ( 1 / 2 ) = 𝑥 → ( ( 1 / 2 ) ∈ ℤ ↔ 𝑥 ∈ ℤ ) )
4	2 3	mtbii	⊢ ( ( 1 / 2 ) = 𝑥 → ¬ 𝑥 ∈ ℤ )
5	4	con2i	⊢ ( 𝑥 ∈ ℤ → ¬ ( 1 / 2 ) = 𝑥 )
6		1cnd	⊢ ( 𝑥 ∈ ℤ → 1 ∈ ℂ )
7		zcn	⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
8		2cnd	⊢ ( 𝑥 ∈ ℤ → 2 ∈ ℂ )
9		2ne0	⊢ 2 ≠ 0
10	9	a1i	⊢ ( 𝑥 ∈ ℤ → 2 ≠ 0 )
11	6 7 8 10	divmul2d	⊢ ( 𝑥 ∈ ℤ → ( ( 1 / 2 ) = 𝑥 ↔ 1 = ( 2 · 𝑥 ) ) )
12	5 11	mtbid	⊢ ( 𝑥 ∈ ℤ → ¬ 1 = ( 2 · 𝑥 ) )
13		eqcom	⊢ ( 2 = ( ( 2 · 𝑥 ) + 1 ) ↔ ( ( 2 · 𝑥 ) + 1 ) = 2 )
14	13	a1i	⊢ ( 𝑥 ∈ ℤ → ( 2 = ( ( 2 · 𝑥 ) + 1 ) ↔ ( ( 2 · 𝑥 ) + 1 ) = 2 ) )
15	8 7	mulcld	⊢ ( 𝑥 ∈ ℤ → ( 2 · 𝑥 ) ∈ ℂ )
16		subadd2	⊢ ( ( 2 ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 2 · 𝑥 ) ∈ ℂ ) → ( ( 2 − 1 ) = ( 2 · 𝑥 ) ↔ ( ( 2 · 𝑥 ) + 1 ) = 2 ) )
17	16	bicomd	⊢ ( ( 2 ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 2 · 𝑥 ) ∈ ℂ ) → ( ( ( 2 · 𝑥 ) + 1 ) = 2 ↔ ( 2 − 1 ) = ( 2 · 𝑥 ) ) )
18	8 6 15 17	syl3anc	⊢ ( 𝑥 ∈ ℤ → ( ( ( 2 · 𝑥 ) + 1 ) = 2 ↔ ( 2 − 1 ) = ( 2 · 𝑥 ) ) )
19		2m1e1	⊢ ( 2 − 1 ) = 1
20	19	a1i	⊢ ( 𝑥 ∈ ℤ → ( 2 − 1 ) = 1 )
21	20	eqeq1d	⊢ ( 𝑥 ∈ ℤ → ( ( 2 − 1 ) = ( 2 · 𝑥 ) ↔ 1 = ( 2 · 𝑥 ) ) )
22	14 18 21	3bitrd	⊢ ( 𝑥 ∈ ℤ → ( 2 = ( ( 2 · 𝑥 ) + 1 ) ↔ 1 = ( 2 · 𝑥 ) ) )
23	12 22	mtbird	⊢ ( 𝑥 ∈ ℤ → ¬ 2 = ( ( 2 · 𝑥 ) + 1 ) )
24	23	nrex	⊢ ¬ ∃ 𝑥 ∈ ℤ 2 = ( ( 2 · 𝑥 ) + 1 )
25	24	intnan	⊢ ¬ ( 2 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 2 = ( ( 2 · 𝑥 ) + 1 ) )
26		eqeq1	⊢ ( 𝑧 = 2 → ( 𝑧 = ( ( 2 · 𝑥 ) + 1 ) ↔ 2 = ( ( 2 · 𝑥 ) + 1 ) ) )
27	26	rexbidv	⊢ ( 𝑧 = 2 → ( ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 2 · 𝑥 ) + 1 ) ↔ ∃ 𝑥 ∈ ℤ 2 = ( ( 2 · 𝑥 ) + 1 ) ) )
28	27 1	elrab2	⊢ ( 2 ∈ 𝑂 ↔ ( 2 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 2 = ( ( 2 · 𝑥 ) + 1 ) ) )
29	25 28	mtbir	⊢ ¬ 2 ∈ 𝑂
30	29	nelir	⊢ 2 ∉ 𝑂