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 ∥ N \to 2 ∥ N$

Step	Hyp	Ref	Expression
1		2z	$⊢ 2 \in ℤ$
2	1	a1i	$⊢ 4 ∥ N \to 2 \in ℤ$
3		4z	$⊢ 4 \in ℤ$
4	3	a1i	$⊢ 4 ∥ N \to 4 \in ℤ$
5		dvdszrcl	$⊢ 4 ∥ N \to (4 \in ℤ \land N \in ℤ)$
6	5	simprd	$⊢ 4 ∥ N \to N \in ℤ$
7	2 4 6	3jca	$⊢ 4 ∥ N \to (2 \in ℤ \land 4 \in ℤ \land N \in ℤ)$
8		z4even	$⊢ 2 ∥ 4$
9	8	jctl	$⊢ 4 ∥ N \to (2 ∥ 4 \land 4 ∥ N)$
10		dvdstr	$⊢ (2 \in ℤ \land 4 \in ℤ \land N \in ℤ) \to ((2 ∥ 4 \land 4 ∥ N) \to 2 ∥ N)$
11	7 9 10	sylc	$⊢ 4 ∥ N \to 2 ∥ N$

Metamath Proof Explorer