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 || N -> 2 || N )

Proof

Step	Hyp	Ref	Expression
1		2z	|- 2 e. ZZ
2	1	a1i	|- ( 4 || N -> 2 e. ZZ )
3		4z	|- 4 e. ZZ
4	3	a1i	|- ( 4 || N -> 4 e. ZZ )
5		dvdszrcl	|- ( 4 || N -> ( 4 e. ZZ /\ N e. ZZ ) )
6	5	simprd	|- ( 4 || N -> N e. ZZ )
7	2 4 6	3jca	|- ( 4 || N -> ( 2 e. ZZ /\ 4 e. ZZ /\ N e. ZZ ) )
8		z4even	|- 2 || 4
9	8	jctl	|- ( 4 || N -> ( 2 || 4 /\ 4 || N ) )
10		dvdstr	|- ( ( 2 e. ZZ /\ 4 e. ZZ /\ N e. ZZ ) -> ( ( 2 || 4 /\ 4 || N ) -> 2 || N ) )
11	7 9 10	sylc	|- ( 4 || N -> 2 || N )