Theorem 0nodd

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

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

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		znegcl	⊢ ( 𝑥 ∈ ℤ → - 𝑥 ∈ ℤ )
6	4 5	nsyl3	⊢ ( 𝑥 ∈ ℤ → ¬ ( 1 / 2 ) = - 𝑥 )
7		eqcom	⊢ ( - 𝑥 = ( 1 / 2 ) ↔ ( 1 / 2 ) = - 𝑥 )
8	6 7	sylnibr	⊢ ( 𝑥 ∈ ℤ → ¬ - 𝑥 = ( 1 / 2 ) )
9		ax-1cn	⊢ 1 ∈ ℂ
10		2cn	⊢ 2 ∈ ℂ
11		2ne0	⊢ 2 ≠ 0
12		divneg	⊢ ( ( 1 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → - ( 1 / 2 ) = ( - 1 / 2 ) )
13	12	eqcomd	⊢ ( ( 1 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( - 1 / 2 ) = - ( 1 / 2 ) )
14	9 10 11 13	mp3an	⊢ ( - 1 / 2 ) = - ( 1 / 2 )
15	14	a1i	⊢ ( 𝑥 ∈ ℤ → ( - 1 / 2 ) = - ( 1 / 2 ) )
16	15	eqeq1d	⊢ ( 𝑥 ∈ ℤ → ( ( - 1 / 2 ) = 𝑥 ↔ - ( 1 / 2 ) = 𝑥 ) )
17		halfcn	⊢ ( 1 / 2 ) ∈ ℂ
18	17	a1i	⊢ ( 𝑥 ∈ ℤ → ( 1 / 2 ) ∈ ℂ )
19		zcn	⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
20	18 19	negcon1d	⊢ ( 𝑥 ∈ ℤ → ( - ( 1 / 2 ) = 𝑥 ↔ - 𝑥 = ( 1 / 2 ) ) )
21	16 20	bitrd	⊢ ( 𝑥 ∈ ℤ → ( ( - 1 / 2 ) = 𝑥 ↔ - 𝑥 = ( 1 / 2 ) ) )
22	8 21	mtbird	⊢ ( 𝑥 ∈ ℤ → ¬ ( - 1 / 2 ) = 𝑥 )
23		neg1cn	⊢ - 1 ∈ ℂ
24	23	a1i	⊢ ( 𝑥 ∈ ℤ → - 1 ∈ ℂ )
25		2cnd	⊢ ( 𝑥 ∈ ℤ → 2 ∈ ℂ )
26	11	a1i	⊢ ( 𝑥 ∈ ℤ → 2 ≠ 0 )
27	24 19 25 26	divmul2d	⊢ ( 𝑥 ∈ ℤ → ( ( - 1 / 2 ) = 𝑥 ↔ - 1 = ( 2 · 𝑥 ) ) )
28	22 27	mtbid	⊢ ( 𝑥 ∈ ℤ → ¬ - 1 = ( 2 · 𝑥 ) )
29		eqcom	⊢ ( 0 = ( ( 2 · 𝑥 ) + 1 ) ↔ ( ( 2 · 𝑥 ) + 1 ) = 0 )
30	29	a1i	⊢ ( 𝑥 ∈ ℤ → ( 0 = ( ( 2 · 𝑥 ) + 1 ) ↔ ( ( 2 · 𝑥 ) + 1 ) = 0 ) )
31		0cnd	⊢ ( 𝑥 ∈ ℤ → 0 ∈ ℂ )
32		1cnd	⊢ ( 𝑥 ∈ ℤ → 1 ∈ ℂ )
33	25 19	mulcld	⊢ ( 𝑥 ∈ ℤ → ( 2 · 𝑥 ) ∈ ℂ )
34		subadd2	⊢ ( ( 0 ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 2 · 𝑥 ) ∈ ℂ ) → ( ( 0 − 1 ) = ( 2 · 𝑥 ) ↔ ( ( 2 · 𝑥 ) + 1 ) = 0 ) )
35	34	bicomd	⊢ ( ( 0 ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 2 · 𝑥 ) ∈ ℂ ) → ( ( ( 2 · 𝑥 ) + 1 ) = 0 ↔ ( 0 − 1 ) = ( 2 · 𝑥 ) ) )
36	31 32 33 35	syl3anc	⊢ ( 𝑥 ∈ ℤ → ( ( ( 2 · 𝑥 ) + 1 ) = 0 ↔ ( 0 − 1 ) = ( 2 · 𝑥 ) ) )
37		df-neg	⊢ - 1 = ( 0 − 1 )
38	37	eqcomi	⊢ ( 0 − 1 ) = - 1
39	38	a1i	⊢ ( 𝑥 ∈ ℤ → ( 0 − 1 ) = - 1 )
40	39	eqeq1d	⊢ ( 𝑥 ∈ ℤ → ( ( 0 − 1 ) = ( 2 · 𝑥 ) ↔ - 1 = ( 2 · 𝑥 ) ) )
41	30 36 40	3bitrd	⊢ ( 𝑥 ∈ ℤ → ( 0 = ( ( 2 · 𝑥 ) + 1 ) ↔ - 1 = ( 2 · 𝑥 ) ) )
42	28 41	mtbird	⊢ ( 𝑥 ∈ ℤ → ¬ 0 = ( ( 2 · 𝑥 ) + 1 ) )
43	42	nrex	⊢ ¬ ∃ 𝑥 ∈ ℤ 0 = ( ( 2 · 𝑥 ) + 1 )
44	43	intnan	⊢ ¬ ( 0 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 0 = ( ( 2 · 𝑥 ) + 1 ) )
45		eqeq1	⊢ ( 𝑧 = 0 → ( 𝑧 = ( ( 2 · 𝑥 ) + 1 ) ↔ 0 = ( ( 2 · 𝑥 ) + 1 ) ) )
46	45	rexbidv	⊢ ( 𝑧 = 0 → ( ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 2 · 𝑥 ) + 1 ) ↔ ∃ 𝑥 ∈ ℤ 0 = ( ( 2 · 𝑥 ) + 1 ) ) )
47	46 1	elrab2	⊢ ( 0 ∈ 𝑂 ↔ ( 0 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 0 = ( ( 2 · 𝑥 ) + 1 ) ) )
48	44 47	mtbir	⊢ ¬ 0 ∈ 𝑂
49	48	nelir	⊢ 0 ∉ 𝑂