Theorem m2even

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

	Ref	Expression
Assertion	m2even	|- ( Z e. ZZ -> ( 2 x. Z ) e. Even )

Proof

Step	Hyp	Ref	Expression
1		2z	|- 2 e. ZZ
2	1	a1i	|- ( Z e. ZZ -> 2 e. ZZ )
3		id	|- ( Z e. ZZ -> Z e. ZZ )
4	2 3	zmulcld	|- ( Z e. ZZ -> ( 2 x. Z ) e. ZZ )
5		dvdsmul1	|- ( ( 2 e. ZZ /\ Z e. ZZ ) -> 2 || ( 2 x. Z ) )
6	1 5	mpan	|- ( Z e. ZZ -> 2 || ( 2 x. Z ) )
7		iseven2	|- ( ( 2 x. Z ) e. Even <-> ( ( 2 x. Z ) e. ZZ /\ 2 || ( 2 x. Z ) ) )
8	4 6 7	sylanbrc	|- ( Z e. ZZ -> ( 2 x. Z ) e. Even )