Theorem m2even

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

	Ref	Expression
Assertion	m2even	⊢ ( 𝑍 ∈ ℤ → ( 2 · 𝑍 ) ∈ Even )

Proof

Step	Hyp	Ref	Expression
1		2z	⊢ 2 ∈ ℤ
2	1	a1i	⊢ ( 𝑍 ∈ ℤ → 2 ∈ ℤ )
3		id	⊢ ( 𝑍 ∈ ℤ → 𝑍 ∈ ℤ )
4	2 3	zmulcld	⊢ ( 𝑍 ∈ ℤ → ( 2 · 𝑍 ) ∈ ℤ )
5		dvdsmul1	⊢ ( ( 2 ∈ ℤ ∧ 𝑍 ∈ ℤ ) → 2 ∥ ( 2 · 𝑍 ) )
6	1 5	mpan	⊢ ( 𝑍 ∈ ℤ → 2 ∥ ( 2 · 𝑍 ) )
7		iseven2	⊢ ( ( 2 · 𝑍 ) ∈ Even ↔ ( ( 2 · 𝑍 ) ∈ ℤ ∧ 2 ∥ ( 2 · 𝑍 ) ) )
8	4 6 7	sylanbrc	⊢ ( 𝑍 ∈ ℤ → ( 2 · 𝑍 ) ∈ Even )