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 ⊢¬12∈ℤ
3 eleq1 ⊢12=x→12∈ℤ↔x∈ℤ
4 2 3 mtbii ⊢12=x→¬x∈ℤ
5 4 con2i ⊢x∈ℤ→¬12=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∈ℤ→12=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