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 ⊢ N ∈ ℤ → 2 ∥ N ↔ N 2 ∈ ℤ

Proof

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