Metamath Proof Explorer

Theorem 2nodd

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

Ref Expression
Hypothesis oddinmgm.e ⊢ O = z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x + 1
Assertion 2nodd ⊢ 2 ∉ O

Proof

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