Metamath Proof Explorer


Theorem m2even

Description: A multiple of 2 is an even number. (Contributed by AV, 5-Jun-2023)

Ref Expression
Assertion m2even Z 2 Z Even

Proof

Step Hyp Ref Expression
1 2z 2
2 1 a1i Z 2
3 id Z Z
4 2 3 zmulcld Z 2 Z
5 dvdsmul1 2 Z 2 2 Z
6 1 5 mpan Z 2 2 Z
7 iseven2 2 Z Even 2 Z 2 2 Z
8 4 6 7 sylanbrc Z 2 Z Even