Metamath Proof Explorer

Theorem 2evenALTV

Description: 2 is an even number. (Contributed by AV, 12-Feb-2020) (Revised by AV, 18-Jun-2020)

Ref Expression
Assertion 2evenALTV 
|- 2 e. Even

Proof

Step Hyp Ref Expression
1 2z 
 |-  2 e. ZZ
2 2div2e1 
 |-  ( 2 / 2 ) = 1
3 1z 
 |-  1 e. ZZ
4 2 3 eqeltri 
 |-  ( 2 / 2 ) e. ZZ
5 iseven 
 |-  ( 2 e. Even <-> ( 2 e. ZZ /\ ( 2 / 2 ) e. ZZ ) )
6 1 4 5 mpbir2an 
 |-  2 e. Even