Theorem nneven

Description: An alternate characterization of an even positive integer. (Contributed by AV, 5-Jun-2023)

	Ref	Expression
Assertion	nneven	|- ( ( N e. NN /\ N e. Even ) -> ( N / 2 ) e. NN )

Proof

Step	Hyp	Ref	Expression
1		nnre	|- ( N e. NN -> N e. RR )
2		2re	|- 2 e. RR
3	2	a1i	|- ( N e. NN -> 2 e. RR )
4		nngt0	|- ( N e. NN -> 0 < N )
5		2pos	|- 0 < 2
6	5	a1i	|- ( N e. NN -> 0 < 2 )
7	1 3 4 6	divgt0d	|- ( N e. NN -> 0 < ( N / 2 ) )
8		evendiv2z	|- ( N e. Even -> ( N / 2 ) e. ZZ )
9	7 8	anim12ci	|- ( ( N e. NN /\ N e. Even ) -> ( ( N / 2 ) e. ZZ /\ 0 < ( N / 2 ) ) )
10		elnnz	|- ( ( N / 2 ) e. NN <-> ( ( N / 2 ) e. ZZ /\ 0 < ( N / 2 ) ) )
11	9 10	sylibr	|- ( ( N e. NN /\ N e. Even ) -> ( N / 2 ) e. NN )