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 4N2N

Proof

Step Hyp Ref Expression
1 2z 2
2 1 a1i 4N2
3 4z 4
4 3 a1i 4N4
5 dvdszrcl 4N4N
6 5 simprd 4NN
7 2 4 6 3jca 4N24N
8 z4even 24
9 8 jctl 4N244N
10 dvdstr 24N244N2N
11 7 9 10 sylc 4N2N