Metamath Proof Explorer


Theorem zeo5

Description: An integer is either even or odd, version of zeo3 avoiding the negation of the representation of an odd number. (Proposed by BJ, 21-Jun-2021.) (Contributed by AV, 26-Jun-2020)

Ref Expression
Assertion zeo5 N2N2N+1

Proof

Step Hyp Ref Expression
1 zeo3 N2N¬2N
2 oddp1even N¬2N2N+1
3 2 bicomd N2N+1¬2N
4 3 orbi2d N2N2N+12N¬2N
5 1 4 mpbird N2N2N+1