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