Metamath Proof Explorer


Theorem evennn2n

Description: A positive integer is even iff it is twice another positive integer. (Contributed by AV, 12-Aug-2021)

Ref Expression
Assertion evennn2n N2Nn2n=N

Proof

Step Hyp Ref Expression
1 eleq1 2n=N2nN
2 simpr 2nnn
3 2re 2
4 3 a1i 2nn2
5 zre nn
6 5 adantl 2nnn
7 0le2 02
8 7 a1i 2nn02
9 nngt0 2n0<2n
10 9 adantr 2nn0<2n
11 prodgt0 2n020<2n0<n
12 4 6 8 10 11 syl22anc 2nn0<n
13 elnnz nn0<n
14 2 12 13 sylanbrc 2nnn
15 14 ex 2nnn
16 1 15 syl6bir 2n=NNnn
17 16 com13 nN2n=Nn
18 17 impcom Nn2n=Nn
19 18 pm4.71rd Nn2n=Nn2n=N
20 19 bicomd Nnn2n=N2n=N
21 20 rexbidva Nnn2n=Nn2n=N
22 nnssz
23 rexss n2n=Nnn2n=N
24 22 23 mp1i Nn2n=Nnn2n=N
25 even2n 2Nn2n=N
26 25 a1i N2Nn2n=N
27 21 24 26 3bitr4rd N2Nn2n=N