Theorem nnehalf

Description: The half of an even positive integer is a positive integer. (Contributed by AV, 28-Jun-2021)

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

Proof

Step	Hyp	Ref	Expression
1		nnnn0	|- ( N e. NN -> N e. NN0 )
2		nn0ehalf	|- ( ( N e. NN0 /\ 2 || N ) -> ( N / 2 ) e. NN0 )
3	1 2	sylan	|- ( ( N e. NN /\ 2 || N ) -> ( N / 2 ) e. NN0 )
4		nn0enne	|- ( N e. NN -> ( ( N / 2 ) e. NN0 <-> ( N / 2 ) e. NN ) )
5	4	adantr	|- ( ( N e. NN /\ 2 || N ) -> ( ( N / 2 ) e. NN0 <-> ( N / 2 ) e. NN ) )
6	3 5	mpbid	|- ( ( N e. NN /\ 2 || N ) -> ( N / 2 ) e. NN )