Metamath Proof Explorer


Theorem nneven

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

Ref Expression
Assertion nneven N N Even N 2

Proof

Step Hyp Ref Expression
1 nnre N N
2 2re 2
3 2 a1i N 2
4 nngt0 N 0 < N
5 2pos 0 < 2
6 5 a1i N 0 < 2
7 1 3 4 6 divgt0d N 0 < N 2
8 evendiv2z N Even N 2
9 7 8 anim12ci N N Even N 2 0 < N 2
10 elnnz N 2 N 2 0 < N 2
11 9 10 sylibr N N Even N 2