Metamath Proof Explorer


Theorem even2n

Description: An integer is even iff it is twice another integer. (Contributed by AV, 25-Jun-2020)

Ref Expression
Assertion even2n 2 N n 2 n = N

Proof

Step Hyp Ref Expression
1 evenelz 2 N N
2 2z 2
3 2 a1i n 2
4 id n n
5 3 4 zmulcld n 2 n
6 5 adantr n 2 n = N 2 n
7 eleq1 2 n = N 2 n N
8 7 adantl n 2 n = N 2 n N
9 6 8 mpbid n 2 n = N N
10 9 rexlimiva n 2 n = N N
11 divides 2 N 2 N n n 2 = N
12 zcn n n
13 2cnd n 2
14 12 13 mulcomd n n 2 = 2 n
15 14 eqeq1d n n 2 = N 2 n = N
16 15 rexbiia n n 2 = N n 2 n = N
17 11 16 bitrdi 2 N 2 N n 2 n = N
18 2 17 mpan N 2 N n 2 n = N
19 1 10 18 pm5.21nii 2 N n 2 n = N