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	⊢ ( 𝑁 ∈ ℤ → ( ( 𝑁 · ( 𝑁 + 1 ) ) / 2 ) ∈ ℤ )

Proof

Step	Hyp	Ref	Expression
1		zeo	⊢ ( 𝑁 ∈ ℤ → ( ( 𝑁 / 2 ) ∈ ℤ ∨ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )
2		peano2z	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 + 1 ) ∈ ℤ )
3		zmulcl	⊢ ( ( ( 𝑁 / 2 ) ∈ ℤ ∧ ( 𝑁 + 1 ) ∈ ℤ ) → ( ( 𝑁 / 2 ) · ( 𝑁 + 1 ) ) ∈ ℤ )
4	2 3	sylan2	⊢ ( ( ( 𝑁 / 2 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑁 / 2 ) · ( 𝑁 + 1 ) ) ∈ ℤ )
5		zcn	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
6	2	zcnd	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 + 1 ) ∈ ℂ )
7		2cnne0	⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
8	7	a1i	⊢ ( 𝑁 ∈ ℤ → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
9		div23	⊢ ( ( 𝑁 ∈ ℂ ∧ ( 𝑁 + 1 ) ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( 𝑁 · ( 𝑁 + 1 ) ) / 2 ) = ( ( 𝑁 / 2 ) · ( 𝑁 + 1 ) ) )
10	5 6 8 9	syl3anc	⊢ ( 𝑁 ∈ ℤ → ( ( 𝑁 · ( 𝑁 + 1 ) ) / 2 ) = ( ( 𝑁 / 2 ) · ( 𝑁 + 1 ) ) )
11	10	eleq1d	⊢ ( 𝑁 ∈ ℤ → ( ( ( 𝑁 · ( 𝑁 + 1 ) ) / 2 ) ∈ ℤ ↔ ( ( 𝑁 / 2 ) · ( 𝑁 + 1 ) ) ∈ ℤ ) )
12	11	adantl	⊢ ( ( ( 𝑁 / 2 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝑁 · ( 𝑁 + 1 ) ) / 2 ) ∈ ℤ ↔ ( ( 𝑁 / 2 ) · ( 𝑁 + 1 ) ) ∈ ℤ ) )
13	4 12	mpbird	⊢ ( ( ( 𝑁 / 2 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑁 · ( 𝑁 + 1 ) ) / 2 ) ∈ ℤ )
14	13	ex	⊢ ( ( 𝑁 / 2 ) ∈ ℤ → ( 𝑁 ∈ ℤ → ( ( 𝑁 · ( 𝑁 + 1 ) ) / 2 ) ∈ ℤ ) )
15		zmulcl	⊢ ( ( 𝑁 ∈ ℤ ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) → ( 𝑁 · ( ( 𝑁 + 1 ) / 2 ) ) ∈ ℤ )
16	15	ancoms	⊢ ( ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 · ( ( 𝑁 + 1 ) / 2 ) ) ∈ ℤ )
17		divass	⊢ ( ( 𝑁 ∈ ℂ ∧ ( 𝑁 + 1 ) ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( 𝑁 · ( 𝑁 + 1 ) ) / 2 ) = ( 𝑁 · ( ( 𝑁 + 1 ) / 2 ) ) )
18	5 6 8 17	syl3anc	⊢ ( 𝑁 ∈ ℤ → ( ( 𝑁 · ( 𝑁 + 1 ) ) / 2 ) = ( 𝑁 · ( ( 𝑁 + 1 ) / 2 ) ) )
19	18	eleq1d	⊢ ( 𝑁 ∈ ℤ → ( ( ( 𝑁 · ( 𝑁 + 1 ) ) / 2 ) ∈ ℤ ↔ ( 𝑁 · ( ( 𝑁 + 1 ) / 2 ) ) ∈ ℤ ) )
20	19	adantl	⊢ ( ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝑁 · ( 𝑁 + 1 ) ) / 2 ) ∈ ℤ ↔ ( 𝑁 · ( ( 𝑁 + 1 ) / 2 ) ) ∈ ℤ ) )
21	16 20	mpbird	⊢ ( ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑁 · ( 𝑁 + 1 ) ) / 2 ) ∈ ℤ )
22	21	ex	⊢ ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ → ( 𝑁 ∈ ℤ → ( ( 𝑁 · ( 𝑁 + 1 ) ) / 2 ) ∈ ℤ ) )
23	14 22	jaoi	⊢ ( ( ( 𝑁 / 2 ) ∈ ℤ ∨ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) → ( 𝑁 ∈ ℤ → ( ( 𝑁 · ( 𝑁 + 1 ) ) / 2 ) ∈ ℤ ) )
24	1 23	mpcom	⊢ ( 𝑁 ∈ ℤ → ( ( 𝑁 · ( 𝑁 + 1 ) ) / 2 ) ∈ ℤ )