Metamath Proof Explorer

Theorem 1neven

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

Ref Expression
Hypothesis 2zrng.e ⊢ E = z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x
Assertion 1neven ⊢ 1 ∉ E

Proof

Step Hyp Ref Expression
1 2zrng.e ⊢ E = z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x
2 halfnz ⊢ ¬ 1 2 ∈ ℤ
3 eleq1a ⊢ x ∈ ℤ → 1 2 = x → 1 2 ∈ ℤ
4 2 3 mtoi ⊢ x ∈ ℤ → ¬ 1 2 = x
5 1cnd ⊢ x ∈ ℤ → 1 ∈ ℂ
6 zcn ⊢ x ∈ ℤ → x ∈ ℂ
7 2cnne0 ⊢ 2 ∈ ℂ ∧ 2 ≠ 0
8 7 a1i ⊢ x ∈ ℤ → 2 ∈ ℂ ∧ 2 ≠ 0
9 divmul2 ⊢ 1 ∈ ℂ ∧ x ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 → 1 2 = x ↔ 1 = 2 ⁢ x
10 5 6 8 9 syl3anc ⊢ x ∈ ℤ → 1 2 = x ↔ 1 = 2 ⁢ x
11 4 10 mtbid ⊢ x ∈ ℤ → ¬ 1 = 2 ⁢ x
12 11 nrex ⊢ ¬ ∃ x ∈ ℤ 1 = 2 ⁢ x
13 12 intnan ⊢ ¬ 1 ∈ ℤ ∧ ∃ x ∈ ℤ 1 = 2 ⁢ x
14 eqeq1 ⊢ z = 1 → z = 2 ⁢ x ↔ 1 = 2 ⁢ x
15 14 rexbidv ⊢ z = 1 → ∃ x ∈ ℤ z = 2 ⁢ x ↔ ∃ x ∈ ℤ 1 = 2 ⁢ x
16 15 1 elrab2 ⊢ 1 ∈ E ↔ 1 ∈ ℤ ∧ ∃ x ∈ ℤ 1 = 2 ⁢ x
17 13 16 mtbir ⊢ ¬ 1 ∈ E
18 17 nelir ⊢ 1 ∉ E