Theorem 1neven

Description: 1 is not an even integer. (Contributed by AV, 12-Feb-2020)

	Ref	Expression
Hypothesis	2zrng.e	⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
Assertion	1neven	⊢ 1 ∉ 𝐸

Proof

Step	Hyp	Ref	Expression
1		2zrng.e	⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
2		halfnz	⊢ ¬ ( 1 / 2 ) ∈ ℤ
3		eleq1a	⊢ ( 𝑥 ∈ ℤ → ( ( 1 / 2 ) = 𝑥 → ( 1 / 2 ) ∈ ℤ ) )
4	2 3	mtoi	⊢ ( 𝑥 ∈ ℤ → ¬ ( 1 / 2 ) = 𝑥 )
5		1cnd	⊢ ( 𝑥 ∈ ℤ → 1 ∈ ℂ )
6		zcn	⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
7		2cnne0	⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
8	7	a1i	⊢ ( 𝑥 ∈ ℤ → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
9		divmul2	⊢ ( ( 1 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( 1 / 2 ) = 𝑥 ↔ 1 = ( 2 · 𝑥 ) ) )
10	5 6 8 9	syl3anc	⊢ ( 𝑥 ∈ ℤ → ( ( 1 / 2 ) = 𝑥 ↔ 1 = ( 2 · 𝑥 ) ) )
11	4 10	mtbid	⊢ ( 𝑥 ∈ ℤ → ¬ 1 = ( 2 · 𝑥 ) )
12	11	nrex	⊢ ¬ ∃ 𝑥 ∈ ℤ 1 = ( 2 · 𝑥 )
13	12	intnan	⊢ ¬ ( 1 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 1 = ( 2 · 𝑥 ) )
14		eqeq1	⊢ ( 𝑧 = 1 → ( 𝑧 = ( 2 · 𝑥 ) ↔ 1 = ( 2 · 𝑥 ) ) )
15	14	rexbidv	⊢ ( 𝑧 = 1 → ( ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) ↔ ∃ 𝑥 ∈ ℤ 1 = ( 2 · 𝑥 ) ) )
16	15 1	elrab2	⊢ ( 1 ∈ 𝐸 ↔ ( 1 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 1 = ( 2 · 𝑥 ) ) )
17	13 16	mtbir	⊢ ¬ 1 ∈ 𝐸
18	17	nelir	⊢ 1 ∉ 𝐸