This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ℤ \to (N \mod 2 = 0 \leftrightarrow 2 ∥ N)$

Step	Hyp	Ref	Expression
1		2nn	$⊢ 2 \in ℕ$
2		dvdsval3	$⊢ (2 \in ℕ \land N \in ℤ) \to (2 ∥ N \leftrightarrow N \mod 2 = 0)$
3	1 2	mpan	$⊢ N \in ℤ \to (2 ∥ N \leftrightarrow N \mod 2 = 0)$
4	3	bicomd	$⊢ N \in ℤ \to (N \mod 2 = 0 \leftrightarrow 2 ∥ N)$