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	|- ( N e. ZZ -> ( 2 || N \/ 2 || ( N + 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		zeo3	|- ( N e. ZZ -> ( 2 || N \/ -. 2 || N ) )
2		oddp1even	|- ( N e. ZZ -> ( -. 2 || N <-> 2 || ( N + 1 ) ) )
3	2	bicomd	|- ( N e. ZZ -> ( 2 || ( N + 1 ) <-> -. 2 || N ) )
4	3	orbi2d	|- ( N e. ZZ -> ( ( 2 || N \/ 2 || ( N + 1 ) ) <-> ( 2 || N \/ -. 2 || N ) ) )
5	1 4	mpbird	|- ( N e. ZZ -> ( 2 || N \/ 2 || ( N + 1 ) ) )