Description: A positive integer is an even nonnegative integer iff it is an even positive integer. (Contributed by AV, 30-May-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | nn0enne | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elnn0 | |
|
2 | nncn | |
|
3 | 2cnd | |
|
4 | 2ne0 | |
|
5 | 4 | a1i | |
6 | 2 3 5 | diveq0ad | |
7 | eleq1 | |
|
8 | 0nnn | |
|
9 | 8 | pm2.21i | |
10 | 7 9 | syl6bi | |
11 | 10 | com12 | |
12 | 6 11 | sylbid | |
13 | 12 | com12 | |
14 | 13 | jao1i | |
15 | 1 14 | sylbi | |
16 | 15 | com12 | |
17 | nnnn0 | |
|
18 | 16 17 | impbid1 | |