This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ∈ ℤ )