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 N2NN2

Proof

Step Hyp Ref Expression
1 2z 2
2 2ne0 20
3 dvdsval2 220N2NN2
4 1 2 3 mp3an12 N2NN2