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	⊢ ( 𝑁 ∈ ℤ → ( ( 𝑁 mod 2 ) = 0 ↔ 2 ∥ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		2nn	⊢ 2 ∈ ℕ
2		dvdsval3	⊢ ( ( 2 ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ( 2 ∥ 𝑁 ↔ ( 𝑁 mod 2 ) = 0 ) )
3	1 2	mpan	⊢ ( 𝑁 ∈ ℤ → ( 2 ∥ 𝑁 ↔ ( 𝑁 mod 2 ) = 0 ) )
4	3	bicomd	⊢ ( 𝑁 ∈ ℤ → ( ( 𝑁 mod 2 ) = 0 ↔ 2 ∥ 𝑁 ) )