Metamath Proof Explorer


Theorem nn0enne

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 NN20N2

Proof

Step Hyp Ref Expression
1 elnn0 N20N2N2=0
2 nncn NN
3 2cnd N2
4 2ne0 20
5 4 a1i N20
6 2 3 5 diveq0ad NN2=0N=0
7 eleq1 N=0N0
8 0nnn ¬0
9 8 pm2.21i 0N2
10 7 9 syl6bi N=0NN2
11 10 com12 NN=0N2
12 6 11 sylbid NN2=0N2
13 12 com12 N2=0NN2
14 13 jao1i N2N2=0NN2
15 1 14 sylbi N20NN2
16 15 com12 NN20N2
17 nnnn0 N2N20
18 16 17 impbid1 NN20N2