Metamath Proof Explorer

Theorem 2even

Description: 2 is 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 2even 
|- 2 e. E

Proof

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