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 ∈ ℤ → N ⁢ N + 1 2 ∈ ℤ

Proof

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