Metamath Proof Explorer


Theorem nnehalf

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

Ref Expression
Assertion nnehalf N2NN2

Proof

Step Hyp Ref Expression
1 nnnn0 NN0
2 nn0ehalf N02NN20
3 1 2 sylan N2NN20
4 nn0enne NN20N2
5 4 adantr N2NN20N2
6 3 5 mpbid N2NN2