m2even

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

		Ref	Expression
	Assertion	m2even	$⊢ Z \in ℤ \to 2 Z \in Even$

Step	Hyp	Ref	Expression
1		2z	$⊢ 2 \in ℤ$
2	1	a1i	$⊢ Z \in ℤ \to 2 \in ℤ$
3		id	$⊢ Z \in ℤ \to Z \in ℤ$
4	2 3	zmulcld	$⊢ Z \in ℤ \to 2 Z \in ℤ$
5		dvdsmul1	$⊢ (2 \in ℤ \land Z \in ℤ) \to 2 ∥ 2 Z$
6	1 5	mpan	$⊢ Z \in ℤ \to 2 ∥ 2 Z$
7		iseven2	$⊢ 2 Z \in Even \leftrightarrow (2 Z \in ℤ \land 2 ∥ 2 Z)$
8	4 6 7	sylanbrc	$⊢ Z \in ℤ \to 2 Z \in Even$

Metamath Proof Explorer