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 e. ZZ | E. x e. ZZ z = ( ( 2 x. x ) + 1 ) }
Assertion 0nodd 
|- 0 e/ O

Proof

Step Hyp Ref Expression
1 oddinmgm.e 
 |-  O = { z e. ZZ | E. x e. ZZ z = ( ( 2 x. x ) + 1 ) }
2 halfnz 
 |-  -. ( 1 / 2 ) e. ZZ
3 eleq1 
 |-  ( ( 1 / 2 ) = -u x -> ( ( 1 / 2 ) e. ZZ <-> -u x e. ZZ ) )
4 2 3 mtbii 
 |-  ( ( 1 / 2 ) = -u x -> -. -u x e. ZZ )
5 znegcl 
 |-  ( x e. ZZ -> -u x e. ZZ )
6 4 5 nsyl3 
 |-  ( x e. ZZ -> -. ( 1 / 2 ) = -u x )
7 eqcom 
 |-  ( -u x = ( 1 / 2 ) <-> ( 1 / 2 ) = -u x )
8 6 7 sylnibr 
 |-  ( x e. ZZ -> -. -u x = ( 1 / 2 ) )
9 ax-1cn 
 |-  1 e. CC
10 2cn 
 |-  2 e. CC
11 2ne0 
 |-  2 =/= 0
12 divneg 
 |-  ( ( 1 e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> -u ( 1 / 2 ) = ( -u 1 / 2 ) )
13 12 eqcomd 
 |-  ( ( 1 e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( -u 1 / 2 ) = -u ( 1 / 2 ) )
14 9 10 11 13 mp3an 
 |-  ( -u 1 / 2 ) = -u ( 1 / 2 )
15 14 a1i 
 |-  ( x e. ZZ -> ( -u 1 / 2 ) = -u ( 1 / 2 ) )
16 15 eqeq1d 
 |-  ( x e. ZZ -> ( ( -u 1 / 2 ) = x <-> -u ( 1 / 2 ) = x ) )
17 halfcn 
 |-  ( 1 / 2 ) e. CC
18 17 a1i 
 |-  ( x e. ZZ -> ( 1 / 2 ) e. CC )
19 zcn 
 |-  ( x e. ZZ -> x e. CC )
20 18 19 negcon1d 
 |-  ( x e. ZZ -> ( -u ( 1 / 2 ) = x <-> -u x = ( 1 / 2 ) ) )
21 16 20 bitrd 
 |-  ( x e. ZZ -> ( ( -u 1 / 2 ) = x <-> -u x = ( 1 / 2 ) ) )
22 8 21 mtbird 
 |-  ( x e. ZZ -> -. ( -u 1 / 2 ) = x )
23 neg1cn 
 |-  -u 1 e. CC
24 23 a1i 
 |-  ( x e. ZZ -> -u 1 e. CC )
25 2cnd 
 |-  ( x e. ZZ -> 2 e. CC )
26 11 a1i 
 |-  ( x e. ZZ -> 2 =/= 0 )
27 24 19 25 26 divmul2d 
 |-  ( x e. ZZ -> ( ( -u 1 / 2 ) = x <-> -u 1 = ( 2 x. x ) ) )
28 22 27 mtbid 
 |-  ( x e. ZZ -> -. -u 1 = ( 2 x. x ) )
29 eqcom 
 |-  ( 0 = ( ( 2 x. x ) + 1 ) <-> ( ( 2 x. x ) + 1 ) = 0 )
30 29 a1i 
 |-  ( x e. ZZ -> ( 0 = ( ( 2 x. x ) + 1 ) <-> ( ( 2 x. x ) + 1 ) = 0 ) )
31 0cnd 
 |-  ( x e. ZZ -> 0 e. CC )
32 1cnd 
 |-  ( x e. ZZ -> 1 e. CC )
33 25 19 mulcld 
 |-  ( x e. ZZ -> ( 2 x. x ) e. CC )
34 subadd2 
 |-  ( ( 0 e. CC /\ 1 e. CC /\ ( 2 x. x ) e. CC ) -> ( ( 0 - 1 ) = ( 2 x. x ) <-> ( ( 2 x. x ) + 1 ) = 0 ) )
35 34 bicomd 
 |-  ( ( 0 e. CC /\ 1 e. CC /\ ( 2 x. x ) e. CC ) -> ( ( ( 2 x. x ) + 1 ) = 0 <-> ( 0 - 1 ) = ( 2 x. x ) ) )
36 31 32 33 35 syl3anc 
 |-  ( x e. ZZ -> ( ( ( 2 x. x ) + 1 ) = 0 <-> ( 0 - 1 ) = ( 2 x. x ) ) )
37 df-neg 
 |-  -u 1 = ( 0 - 1 )
38 37 eqcomi 
 |-  ( 0 - 1 ) = -u 1
39 38 a1i 
 |-  ( x e. ZZ -> ( 0 - 1 ) = -u 1 )
40 39 eqeq1d 
 |-  ( x e. ZZ -> ( ( 0 - 1 ) = ( 2 x. x ) <-> -u 1 = ( 2 x. x ) ) )
41 30 36 40 3bitrd 
 |-  ( x e. ZZ -> ( 0 = ( ( 2 x. x ) + 1 ) <-> -u 1 = ( 2 x. x ) ) )
42 28 41 mtbird 
 |-  ( x e. ZZ -> -. 0 = ( ( 2 x. x ) + 1 ) )
43 42 nrex 
 |-  -. E. x e. ZZ 0 = ( ( 2 x. x ) + 1 )
44 43 intnan 
 |-  -. ( 0 e. ZZ /\ E. x e. ZZ 0 = ( ( 2 x. x ) + 1 ) )
45 eqeq1 
 |-  ( z = 0 -> ( z = ( ( 2 x. x ) + 1 ) <-> 0 = ( ( 2 x. x ) + 1 ) ) )
46 45 rexbidv 
 |-  ( z = 0 -> ( E. x e. ZZ z = ( ( 2 x. x ) + 1 ) <-> E. x e. ZZ 0 = ( ( 2 x. x ) + 1 ) ) )
47 46 1 elrab2 
 |-  ( 0 e. O <-> ( 0 e. ZZ /\ E. x e. ZZ 0 = ( ( 2 x. x ) + 1 ) ) )
48 44 47 mtbir 
 |-  -. 0 e. O
49 48 nelir 
 |-  0 e/ O