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 
|- 2 || 4

Proof

Step Hyp Ref Expression
1 2z 
 |-  2 e. ZZ
2 dvdsmul1 
 |-  ( ( 2 e. ZZ /\ 2 e. ZZ ) -> 2 || ( 2 x. 2 ) )
3 1 1 2 mp2an 
 |-  2 || ( 2 x. 2 )
4 2t2e4 
 |-  ( 2 x. 2 ) = 4
5 3 4 breqtri 
 |-  2 || 4