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 ∥ 𝑁 )