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 
|- ( N e. ZZ -> ( ( N x. ( N + 1 ) ) / 2 ) e. ZZ )

Proof

Step Hyp Ref Expression
1 zeo 
 |-  ( N e. ZZ -> ( ( N / 2 ) e. ZZ \/ ( ( N + 1 ) / 2 ) e. ZZ ) )
2 peano2z 
 |-  ( N e. ZZ -> ( N + 1 ) e. ZZ )
3 zmulcl 
 |-  ( ( ( N / 2 ) e. ZZ /\ ( N + 1 ) e. ZZ ) -> ( ( N / 2 ) x. ( N + 1 ) ) e. ZZ )
4 2 3 sylan2 
 |-  ( ( ( N / 2 ) e. ZZ /\ N e. ZZ ) -> ( ( N / 2 ) x. ( N + 1 ) ) e. ZZ )
5 zcn 
 |-  ( N e. ZZ -> N e. CC )
6 2 zcnd 
 |-  ( N e. ZZ -> ( N + 1 ) e. CC )
7 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
8 7 a1i 
 |-  ( N e. ZZ -> ( 2 e. CC /\ 2 =/= 0 ) )
9 div23 
 |-  ( ( N e. CC /\ ( N + 1 ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( N x. ( N + 1 ) ) / 2 ) = ( ( N / 2 ) x. ( N + 1 ) ) )
10 5 6 8 9 syl3anc 
 |-  ( N e. ZZ -> ( ( N x. ( N + 1 ) ) / 2 ) = ( ( N / 2 ) x. ( N + 1 ) ) )
11 10 eleq1d 
 |-  ( N e. ZZ -> ( ( ( N x. ( N + 1 ) ) / 2 ) e. ZZ <-> ( ( N / 2 ) x. ( N + 1 ) ) e. ZZ ) )
12 11 adantl 
 |-  ( ( ( N / 2 ) e. ZZ /\ N e. ZZ ) -> ( ( ( N x. ( N + 1 ) ) / 2 ) e. ZZ <-> ( ( N / 2 ) x. ( N + 1 ) ) e. ZZ ) )
13 4 12 mpbird 
 |-  ( ( ( N / 2 ) e. ZZ /\ N e. ZZ ) -> ( ( N x. ( N + 1 ) ) / 2 ) e. ZZ )
14 13 ex 
 |-  ( ( N / 2 ) e. ZZ -> ( N e. ZZ -> ( ( N x. ( N + 1 ) ) / 2 ) e. ZZ ) )
15 zmulcl 
 |-  ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( N x. ( ( N + 1 ) / 2 ) ) e. ZZ )
16 15 ancoms 
 |-  ( ( ( ( N + 1 ) / 2 ) e. ZZ /\ N e. ZZ ) -> ( N x. ( ( N + 1 ) / 2 ) ) e. ZZ )
17 divass 
 |-  ( ( N e. CC /\ ( N + 1 ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( N x. ( N + 1 ) ) / 2 ) = ( N x. ( ( N + 1 ) / 2 ) ) )
18 5 6 8 17 syl3anc 
 |-  ( N e. ZZ -> ( ( N x. ( N + 1 ) ) / 2 ) = ( N x. ( ( N + 1 ) / 2 ) ) )
19 18 eleq1d 
 |-  ( N e. ZZ -> ( ( ( N x. ( N + 1 ) ) / 2 ) e. ZZ <-> ( N x. ( ( N + 1 ) / 2 ) ) e. ZZ ) )
20 19 adantl 
 |-  ( ( ( ( N + 1 ) / 2 ) e. ZZ /\ N e. ZZ ) -> ( ( ( N x. ( N + 1 ) ) / 2 ) e. ZZ <-> ( N x. ( ( N + 1 ) / 2 ) ) e. ZZ ) )
21 16 20 mpbird 
 |-  ( ( ( ( N + 1 ) / 2 ) e. ZZ /\ N e. ZZ ) -> ( ( N x. ( N + 1 ) ) / 2 ) e. ZZ )
22 21 ex 
 |-  ( ( ( N + 1 ) / 2 ) e. ZZ -> ( N e. ZZ -> ( ( N x. ( N + 1 ) ) / 2 ) e. ZZ ) )
23 14 22 jaoi 
 |-  ( ( ( N / 2 ) e. ZZ \/ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( N e. ZZ -> ( ( N x. ( N + 1 ) ) / 2 ) e. ZZ ) )
24 1 23 mpcom 
 |-  ( N e. ZZ -> ( ( N x. ( N + 1 ) ) / 2 ) e. ZZ )