Metamath Proof Explorer


Theorem evennn02n

Description: A nonnegative integer is even iff it is twice another nonnegative integer. (Contributed by AV, 12-Aug-2021) (Proof shortened by AV, 10-Jul-2022)

Ref Expression
Assertion evennn02n N02Nn02n=N

Proof

Step Hyp Ref Expression
1 eleq1 2n=N2n0N0
2 simpr 2n0nn
3 2rp 2+
4 3 a1i 2n0n2+
5 zre nn
6 5 adantl 2n0nn
7 nn0ge0 2n002n
8 7 adantr 2n0n02n
9 4 6 8 prodge0rd 2n0n0n
10 elnn0z n0n0n
11 2 9 10 sylanbrc 2n0nn0
12 11 ex 2n0nn0
13 1 12 syl6bir 2n=NN0nn0
14 13 com13 nN02n=Nn0
15 14 impcom N0n2n=Nn0
16 15 pm4.71rd N0n2n=Nn02n=N
17 16 bicomd N0nn02n=N2n=N
18 17 rexbidva N0nn02n=Nn2n=N
19 nn0ssz 0
20 rexss 0n02n=Nnn02n=N
21 19 20 mp1i N0n02n=Nnn02n=N
22 even2n 2Nn2n=N
23 22 a1i N02Nn2n=N
24 18 21 23 3bitr4rd N02Nn02n=N