Metamath Proof Explorer

Theorem m2even

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

Ref Expression
Assertion m2even ⊢ Z ∈ ℤ → 2 ⁢ Z ∈ Even

Proof

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