Theorem mod2eq0even

Description: An integer is 0 modulo 2 iff it is even (i.e. divisible by 2), see example 2 in ApostolNT p. 107. (Contributed by AV, 21-Jul-2021)

	Ref	Expression
Assertion	mod2eq0even	$$⊢N\in \mathbb{Z}\to \left(N\mathrm{mod}2=0\leftrightarrow 2\parallel N\right)$$

Proof

Step	Hyp	Ref	Expression
1		2nn	$$⊢2\in \mathbb{N}$$
2		dvdsval3	$$⊢\left(2\in \mathbb{N}\wedge N\in \mathbb{Z}\right)\to \left(2\parallel N\leftrightarrow N\mathrm{mod}2=0\right)$$
3	1 2	mpan	$$⊢N\in \mathbb{Z}\to \left(2\parallel N\leftrightarrow N\mathrm{mod}2=0\right)$$
4	3	bicomd	$$⊢N\in \mathbb{Z}\to \left(N\mathrm{mod}2=0\leftrightarrow 2\parallel N\right)$$