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

Metamath Proof Explorer

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 ) ∈ ℤ ) )