Metamath Proof Explorer

Theorem z0even

Description: 2 divides 0. That means 0 is even. (Contributed by AV, 11-Feb-2020) (Revised by AV, 23-Jun-2021)

Ref Expression
Assertion z0even 
|- 2 || 0

Proof

Step Hyp Ref Expression
1 2z 
 |-  2 e. ZZ
2 dvds0 
 |-  ( 2 e. ZZ -> 2 || 0 )
3 1 2 ax-mp 
 |-  2 || 0