Description: An alternate characterization of an even positive integer. (Contributed by AV, 5-Jun-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | nneven |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnre | ||
2 | 2re | ||
3 | 2 | a1i | |
4 | nngt0 | ||
5 | 2pos | ||
6 | 5 | a1i | |
7 | 1 3 4 6 | divgt0d | |
8 | evendiv2z | ||
9 | 7 8 | anim12ci | |
10 | elnnz | ||
11 | 9 10 | sylibr |