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 ⊢¬12∈ℤ
3 eleq1 ⊢12=−x→12∈ℤ↔−x∈ℤ
4 2 3 mtbii ⊢12=−x→¬−x∈ℤ
5 znegcl ⊢x∈ℤ→−x∈ℤ
6 4 5 nsyl3 ⊢x∈ℤ→¬12=−x
7 eqcom ⊢−x=12↔12=−x
8 6 7 sylnibr ⊢x∈ℤ→¬−x=12
9 ax-1cn ⊢1∈ℂ
10 2cn ⊢2∈ℂ
11 2ne0 ⊢2≠0
12 divneg ⊢1∈ℂ∧2∈ℂ∧2≠0→−12=−12
13 12 eqcomd ⊢1∈ℂ∧2∈ℂ∧2≠0→−12=−12
14 9 10 11 13 mp3an ⊢−12=−12
15 14 a1i ⊢x∈ℤ→−12=−12
16 15 eqeq1d ⊢x∈ℤ→−12=x↔−12=x
17 halfcn ⊢12∈ℂ
18 17 a1i ⊢x∈ℤ→12∈ℂ
19 zcn ⊢x∈ℤ→x∈ℂ
20 18 19 negcon1d ⊢x∈ℤ→−12=x↔−x=12
21 16 20 bitrd ⊢x∈ℤ→−12=x↔−x=12
22 8 21 mtbird ⊢x∈ℤ→¬−12=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∈ℤ→−12=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