Metamath Proof Explorer


Theorem z4even

Description: 2 divides 4. That means 4 is even. (Contributed by AV, 23-Jul-2020) (Revised by AV, 4-Jul-2021)

Ref Expression
Assertion z4even 24

Proof

Step Hyp Ref Expression
1 2z 2
2 dvdsmul1 22222
3 1 1 2 mp2an 222
4 2t2e4 22=4
5 3 4 breqtri 24