Metamath Proof Explorer

Theorem 0nodd

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

Ref Expression
Hypothesis oddinmgm.e ⊢ O = z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x + 1
Assertion 0nodd ⊢ 0 ∉ 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 znegcl ⊢ x ∈ ℤ → − x ∈ ℤ
6 4 5 nsyl3 ⊢ x ∈ ℤ → ¬ 1 2 = − x
7 eqcom ⊢ − x = 1 2 ↔ 1 2 = − x
8 6 7 sylnibr ⊢ x ∈ ℤ → ¬ − x = 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 ⊢ x ∈ ℤ → − 1 2 = − 1 2
16 15 eqeq1d ⊢ x ∈ ℤ → − 1 2 = x ↔ − 1 2 = x
17 halfcn ⊢ 1 2 ∈ ℂ
18 17 a1i ⊢ x ∈ ℤ → 1 2 ∈ ℂ
19 zcn ⊢ x ∈ ℤ → x ∈ ℂ
20 18 19 negcon1d ⊢ x ∈ ℤ → − 1 2 = x ↔ − x = 1 2
21 16 20 bitrd ⊢ x ∈ ℤ → − 1 2 = x ↔ − x = 1 2
22 8 21 mtbird ⊢ x ∈ ℤ → ¬ − 1 2 = x
23 neg1cn ⊢ − 1 ∈ ℂ
24 23 a1i ⊢ x ∈ ℤ → − 1 ∈ ℂ
25 2cnd ⊢ x ∈ ℤ → 2 ∈ ℂ
26 11 a1i ⊢ x ∈ ℤ → 2 ≠ 0
27 24 19 25 26 divmul2d ⊢ x ∈ ℤ → − 1 2 = x ↔ − 1 = 2 ⁢ x
28 22 27 mtbid ⊢ x ∈ ℤ → ¬ − 1 = 2 ⁢ x
29 eqcom ⊢ 0 = 2 ⁢ x + 1 ↔ 2 ⁢ x + 1 = 0
30 29 a1i ⊢ x ∈ ℤ → 0 = 2 ⁢ x + 1 ↔ 2 ⁢ x + 1 = 0
31 0cnd ⊢ x ∈ ℤ → 0 ∈ ℂ
32 1cnd ⊢ x ∈ ℤ → 1 ∈ ℂ
33 25 19 mulcld ⊢ x ∈ ℤ → 2 ⁢ x ∈ ℂ
34 subadd2 ⊢ 0 ∈ ℂ ∧ 1 ∈ ℂ ∧ 2 ⁢ x ∈ ℂ → 0 − 1 = 2 ⁢ x ↔ 2 ⁢ x + 1 = 0
35 34 bicomd ⊢ 0 ∈ ℂ ∧ 1 ∈ ℂ ∧ 2 ⁢ x ∈ ℂ → 2 ⁢ x + 1 = 0 ↔ 0 − 1 = 2 ⁢ x
36 31 32 33 35 syl3anc ⊢ x ∈ ℤ → 2 ⁢ x + 1 = 0 ↔ 0 − 1 = 2 ⁢ x
37 df-neg ⊢ − 1 = 0 − 1
38 37 eqcomi ⊢ 0 − 1 = − 1
39 38 a1i ⊢ x ∈ ℤ → 0 − 1 = − 1
40 39 eqeq1d ⊢ x ∈ ℤ → 0 − 1 = 2 ⁢ x ↔ − 1 = 2 ⁢ x
41 30 36 40 3bitrd ⊢ x ∈ ℤ → 0 = 2 ⁢ x + 1 ↔ − 1 = 2 ⁢ x
42 28 41 mtbird ⊢ x ∈ ℤ → ¬ 0 = 2 ⁢ x + 1
43 42 nrex ⊢ ¬ ∃ x ∈ ℤ 0 = 2 ⁢ x + 1
44 43 intnan ⊢ ¬ 0 ∈ ℤ ∧ ∃ x ∈ ℤ 0 = 2 ⁢ x + 1
45 eqeq1 ⊢ z = 0 → z = 2 ⁢ x + 1 ↔ 0 = 2 ⁢ x + 1
46 45 rexbidv ⊢ z = 0 → ∃ x ∈ ℤ z = 2 ⁢ x + 1 ↔ ∃ x ∈ ℤ 0 = 2 ⁢ x + 1
47 46 1 elrab2 ⊢ 0 ∈ O ↔ 0 ∈ ℤ ∧ ∃ x ∈ ℤ 0 = 2 ⁢ x + 1
48 44 47 mtbir ⊢ ¬ 0 ∈ O
49 48 nelir ⊢ 0 ∉ O