Metamath Proof Explorer

Theorem mod2eq0even

Description: An integer is 0 modulo 2 iff it is even (i.e. divisible by 2), see example 2 in ApostolNT p. 107. (Contributed by AV, 21-Jul-2021)

Ref Expression
Assertion mod2eq0even 
|- ( N e. ZZ -> ( ( N mod 2 ) = 0 <-> 2 || N ) )

Proof

Step Hyp Ref Expression
1 2nn 
 |-  2 e. NN
2 dvdsval3 
 |-  ( ( 2 e. NN /\ N e. ZZ ) -> ( 2 || N <-> ( N mod 2 ) = 0 ) )
3 1 2 mpan 
 |-  ( N e. ZZ -> ( 2 || N <-> ( N mod 2 ) = 0 ) )
4 3 bicomd 
 |-  ( N e. ZZ -> ( ( N mod 2 ) = 0 <-> 2 || N ) )