Metamath Proof Explorer

Theorem 0even

Description: 0 is an even integer. (Contributed by AV, 11-Feb-2020)

Ref Expression
Hypothesis 2zrng.e 
|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }
Assertion 0even 
|- 0 e. E

Proof

Step Hyp Ref Expression
1 2zrng.e 
 |-  E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }
2 0z 
 |-  0 e. ZZ
3 2cn 
 |-  2 e. CC
4 0zd 
 |-  ( 2 e. CC -> 0 e. ZZ )
5 oveq2 
 |-  ( x = 0 -> ( 2 x. x ) = ( 2 x. 0 ) )
6 5 eqeq2d 
 |-  ( x = 0 -> ( 0 = ( 2 x. x ) <-> 0 = ( 2 x. 0 ) ) )
7 6 adantl 
 |-  ( ( 2 e. CC /\ x = 0 ) -> ( 0 = ( 2 x. x ) <-> 0 = ( 2 x. 0 ) ) )
8 mul01 
 |-  ( 2 e. CC -> ( 2 x. 0 ) = 0 )
9 8 eqcomd 
 |-  ( 2 e. CC -> 0 = ( 2 x. 0 ) )
10 4 7 9 rspcedvd 
 |-  ( 2 e. CC -> E. x e. ZZ 0 = ( 2 x. x ) )
11 3 10 ax-mp 
 |-  E. x e. ZZ 0 = ( 2 x. x )
12 eqeq1 
 |-  ( z = 0 -> ( z = ( 2 x. x ) <-> 0 = ( 2 x. x ) ) )
13 12 rexbidv 
 |-  ( z = 0 -> ( E. x e. ZZ z = ( 2 x. x ) <-> E. x e. ZZ 0 = ( 2 x. x ) ) )
14 13 elrab 
 |-  ( 0 e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } <-> ( 0 e. ZZ /\ E. x e. ZZ 0 = ( 2 x. x ) ) )
15 2 11 14 mpbir2an 
 |-  0 e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }
16 15 1 eleqtrri 
 |-  0 e. E