Theorem evend2

Description: An integer is even iff its quotient with 2 is an integer. This is a representation of even numbers without using the divides relation, see zeo and zeo2 . (Contributed by AV, 22-Jun-2021)

	Ref	Expression
Assertion	evend2	⊢ ( 𝑁 ∈ ℤ → ( 2 ∥ 𝑁 ↔ ( 𝑁 / 2 ) ∈ ℤ ) )

Proof

Step	Hyp	Ref	Expression
1		2z	⊢ 2 ∈ ℤ
2		2ne0	⊢ 2 ≠ 0
3		dvdsval2	⊢ ( ( 2 ∈ ℤ ∧ 2 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 2 ∥ 𝑁 ↔ ( 𝑁 / 2 ) ∈ ℤ ) )
4	1 2 3	mp3an12	⊢ ( 𝑁 ∈ ℤ → ( 2 ∥ 𝑁 ↔ ( 𝑁 / 2 ) ∈ ℤ ) )