Metamath Proof Explorer


Theorem nnennex

Description: For each even positive integer there is a positive integer which, multiplied by 2, results in the even positive integer. (Contributed by AV, 5-Jun-2023)

Ref Expression
Assertion nnennex N N 2 m N = 2 m

Proof

Step Hyp Ref Expression
1 simpr N N 2 N 2
2 oveq2 m = N 2 2 m = 2 N 2
3 2 eqeq2d m = N 2 N = 2 m N = 2 N 2
4 3 adantl N N 2 m = N 2 N = 2 m N = 2 N 2
5 nncn N N
6 2cnd N 2
7 2ne0 2 0
8 7 a1i N 2 0
9 divcan2 N 2 2 0 2 N 2 = N
10 9 eqcomd N 2 2 0 N = 2 N 2
11 5 6 8 10 syl3anc N N = 2 N 2
12 11 adantr N N 2 N = 2 N 2
13 1 4 12 rspcedvd N N 2 m N = 2 m