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