This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 4dvdseven

Description: An integer which is divisible by 4 is divisible by 2, that is, is even. (Contributed by AV, 4-Jul-2021)

Ref Expression
Assertion 4dvdseven ( 4 ∥ 𝑁 → 2 ∥ 𝑁 )

Proof

Step Hyp Ref Expression
1 2z ⊢ 2 ∈ ℤ
2 1 a1i ⊢ ( 4 ∥ 𝑁 → 2 ∈ ℤ )
3 4z ⊢ 4 ∈ ℤ
4 3 a1i ⊢ ( 4 ∥ 𝑁 → 4 ∈ ℤ )
5 dvdszrcl ⊢ ( 4 ∥ 𝑁 → ( 4 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
6 5 simprd ⊢ ( 4 ∥ 𝑁 → 𝑁 ∈ ℤ )
7 2 4 6 3jca ⊢ ( 4 ∥ 𝑁 → ( 2 ∈ ℤ ∧ 4 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
8 z4even ⊢ 2 ∥ 4
9 8 jctl ⊢ ( 4 ∥ 𝑁 → ( 2 ∥ 4 ∧ 4 ∥ 𝑁 ) )
10 dvdstr ⊢ ( ( 2 ∈ ℤ ∧ 4 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 2 ∥ 4 ∧ 4 ∥ 𝑁 ) → 2 ∥ 𝑁 ) )
11 7 9 10 sylc ⊢ ( 4 ∥ 𝑁 → 2 ∥ 𝑁 )