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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zeo | |
|
2 | peano2z | |
|
3 | zmulcl | |
|
4 | 2 3 | sylan2 | |
5 | zcn | |
|
6 | 2 | zcnd | |
7 | 2cnne0 | |
|
8 | 7 | a1i | |
9 | div23 | |
|
10 | 5 6 8 9 | syl3anc | |
11 | 10 | eleq1d | |
12 | 11 | adantl | |
13 | 4 12 | mpbird | |
14 | 13 | ex | |
15 | zmulcl | |
|
16 | 15 | ancoms | |
17 | divass | |
|
18 | 5 6 8 17 | syl3anc | |
19 | 18 | eleq1d | |
20 | 19 | adantl | |
21 | 16 20 | mpbird | |
22 | 21 | ex | |
23 | 14 22 | jaoi | |
24 | 1 23 | mpcom | |