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