Metamath Proof Explorer


Theorem mulsucdiv2z

Description: An integer multiplied with its successor divided by 2 yields an integer, i.e. an integer multiplied with its successor is even. (Contributed by AV, 19-Jul-2021)

Ref Expression
Assertion mulsucdiv2z NNN+12

Proof

Step Hyp Ref Expression
1 zeo NN2N+12
2 peano2z NN+1
3 zmulcl N2N+1N2N+1
4 2 3 sylan2 N2NN2N+1
5 zcn NN
6 2 zcnd NN+1
7 2cnne0 220
8 7 a1i N220
9 div23 NN+1220NN+12=N2N+1
10 5 6 8 9 syl3anc NNN+12=N2N+1
11 10 eleq1d NNN+12N2N+1
12 11 adantl N2NNN+12N2N+1
13 4 12 mpbird N2NNN+12
14 13 ex N2NNN+12
15 zmulcl NN+12NN+12
16 15 ancoms N+12NNN+12
17 divass NN+1220NN+12=NN+12
18 5 6 8 17 syl3anc NNN+12=NN+12
19 18 eleq1d NNN+12NN+12
20 19 adantl N+12NNN+12NN+12
21 16 20 mpbird N+12NNN+12
22 21 ex N+12NNN+12
23 14 22 jaoi N2N+12NNN+12
24 1 23 mpcom NNN+12