Metamath Proof Explorer

Theorem 1neven

Description: 1 is not an even integer. (Contributed by AV, 12-Feb-2020)

Ref Expression
Hypothesis 2zrng.e 
|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }
Assertion 1neven 
|- 1 e/ E

Proof

Step Hyp Ref Expression
1 2zrng.e 
 |-  E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }
2 halfnz 
 |-  -. ( 1 / 2 ) e. ZZ
3 eleq1a 
 |-  ( x e. ZZ -> ( ( 1 / 2 ) = x -> ( 1 / 2 ) e. ZZ ) )
4 2 3 mtoi 
 |-  ( x e. ZZ -> -. ( 1 / 2 ) = x )
5 1cnd 
 |-  ( x e. ZZ -> 1 e. CC )
6 zcn 
 |-  ( x e. ZZ -> x e. CC )
7 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
8 7 a1i 
 |-  ( x e. ZZ -> ( 2 e. CC /\ 2 =/= 0 ) )
9 divmul2 
 |-  ( ( 1 e. CC /\ x e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( 1 / 2 ) = x <-> 1 = ( 2 x. x ) ) )
10 5 6 8 9 syl3anc 
 |-  ( x e. ZZ -> ( ( 1 / 2 ) = x <-> 1 = ( 2 x. x ) ) )
11 4 10 mtbid 
 |-  ( x e. ZZ -> -. 1 = ( 2 x. x ) )
12 11 nrex 
 |-  -. E. x e. ZZ 1 = ( 2 x. x )
13 12 intnan 
 |-  -. ( 1 e. ZZ /\ E. x e. ZZ 1 = ( 2 x. x ) )
14 eqeq1 
 |-  ( z = 1 -> ( z = ( 2 x. x ) <-> 1 = ( 2 x. x ) ) )
15 14 rexbidv 
 |-  ( z = 1 -> ( E. x e. ZZ z = ( 2 x. x ) <-> E. x e. ZZ 1 = ( 2 x. x ) ) )
16 15 1 elrab2 
 |-  ( 1 e. E <-> ( 1 e. ZZ /\ E. x e. ZZ 1 = ( 2 x. x ) ) )
17 13 16 mtbir 
 |-  -. 1 e. E
18 17 nelir 
 |-  1 e/ E