| Step | Hyp | Ref
| Expression |
| 1 | | elnn0 12528 |
. 2
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℕ
∨ 𝑁 =
0)) |
| 2 | | 1zzd 12648 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 1 ∈
ℤ) |
| 3 | | nnz 12634 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
| 4 | | elfzelz 13564 |
. . . . . . . 8
⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℤ) |
| 5 | 4 | zcnd 12723 |
. . . . . . 7
⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℂ) |
| 6 | 5 | adantl 481 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → 𝑘 ∈ ℂ) |
| 7 | | id 22 |
. . . . . 6
⊢ (𝑘 = (𝑗 + 1) → 𝑘 = (𝑗 + 1)) |
| 8 | 2, 2, 3, 6, 7 | fsumshftm 15817 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ (1...𝑁)𝑘 = Σ𝑗 ∈ ((1 − 1)...(𝑁 − 1))(𝑗 + 1)) |
| 9 | | 1m1e0 12338 |
. . . . . . 7
⊢ (1
− 1) = 0 |
| 10 | 9 | oveq1i 7441 |
. . . . . 6
⊢ ((1
− 1)...(𝑁 − 1))
= (0...(𝑁 −
1)) |
| 11 | 10 | sumeq1i 15733 |
. . . . 5
⊢
Σ𝑗 ∈ ((1
− 1)...(𝑁 −
1))(𝑗 + 1) = Σ𝑗 ∈ (0...(𝑁 − 1))(𝑗 + 1) |
| 12 | 8, 11 | eqtrdi 2793 |
. . . 4
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ (1...𝑁)𝑘 = Σ𝑗 ∈ (0...(𝑁 − 1))(𝑗 + 1)) |
| 13 | | elfznn0 13660 |
. . . . . . . . 9
⊢ (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 ∈ ℕ0) |
| 14 | 13 | adantl 481 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑗 ∈ ℕ0) |
| 15 | | bcnp1n 14353 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ0
→ ((𝑗 + 1)C𝑗) = (𝑗 + 1)) |
| 16 | 14, 15 | syl 17 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑗 + 1)C𝑗) = (𝑗 + 1)) |
| 17 | 14 | nn0cnd 12589 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑗 ∈ ℂ) |
| 18 | | ax-1cn 11213 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
| 19 | | addcom 11447 |
. . . . . . . . 9
⊢ ((𝑗 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑗 + 1) =
(1 + 𝑗)) |
| 20 | 17, 18, 19 | sylancl 586 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑗 + 1) = (1 + 𝑗)) |
| 21 | 20 | oveq1d 7446 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑗 + 1)C𝑗) = ((1 + 𝑗)C𝑗)) |
| 22 | 16, 21 | eqtr3d 2779 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑗 + 1) = ((1 + 𝑗)C𝑗)) |
| 23 | 22 | sumeq2dv 15738 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈ (0...(𝑁 − 1))(𝑗 + 1) = Σ𝑗 ∈ (0...(𝑁 − 1))((1 + 𝑗)C𝑗)) |
| 24 | | 1nn0 12542 |
. . . . . 6
⊢ 1 ∈
ℕ0 |
| 25 | | nnm1nn0 12567 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
| 26 | | bcxmas 15871 |
. . . . . 6
⊢ ((1
∈ ℕ0 ∧ (𝑁 − 1) ∈ ℕ0)
→ (((1 + 1) + (𝑁
− 1))C(𝑁 − 1))
= Σ𝑗 ∈
(0...(𝑁 − 1))((1 +
𝑗)C𝑗)) |
| 27 | 24, 25, 26 | sylancr 587 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (((1 + 1)
+ (𝑁 − 1))C(𝑁 − 1)) = Σ𝑗 ∈ (0...(𝑁 − 1))((1 + 𝑗)C𝑗)) |
| 28 | 23, 27 | eqtr4d 2780 |
. . . 4
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈ (0...(𝑁 − 1))(𝑗 + 1) = (((1 + 1) + (𝑁 − 1))C(𝑁 − 1))) |
| 29 | | 1cnd 11256 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 1 ∈
ℂ) |
| 30 | | nncn 12274 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
| 31 | 29, 29, 30 | ppncand 11660 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → ((1 + 1)
+ (𝑁 − 1)) = (1 +
𝑁)) |
| 32 | 29, 30, 31 | comraddd 11475 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → ((1 + 1)
+ (𝑁 − 1)) = (𝑁 + 1)) |
| 33 | 32 | oveq1d 7446 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (((1 + 1)
+ (𝑁 − 1))C(𝑁 − 1)) = ((𝑁 + 1)C(𝑁 − 1))) |
| 34 | | nnnn0 12533 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
| 35 | | bcp1m1 14359 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1)C(𝑁 − 1)) = (((𝑁 + 1) · 𝑁) / 2)) |
| 36 | 34, 35 | syl 17 |
. . . . 5
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1)C(𝑁 − 1)) = (((𝑁 + 1) · 𝑁) / 2)) |
| 37 | | sqval 14155 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℂ → (𝑁↑2) = (𝑁 · 𝑁)) |
| 38 | 37 | eqcomd 2743 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℂ → (𝑁 · 𝑁) = (𝑁↑2)) |
| 39 | | mullid 11260 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℂ → (1
· 𝑁) = 𝑁) |
| 40 | 38, 39 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝑁 ∈ ℂ → ((𝑁 · 𝑁) + (1 · 𝑁)) = ((𝑁↑2) + 𝑁)) |
| 41 | 30, 40 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → ((𝑁 · 𝑁) + (1 · 𝑁)) = ((𝑁↑2) + 𝑁)) |
| 42 | 30, 30, 29, 41 | joinlmuladdmuld 11288 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) · 𝑁) = ((𝑁↑2) + 𝑁)) |
| 43 | 42 | oveq1d 7446 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) · 𝑁) / 2) = (((𝑁↑2) + 𝑁) / 2)) |
| 44 | 33, 36, 43 | 3eqtrd 2781 |
. . . 4
⊢ (𝑁 ∈ ℕ → (((1 + 1)
+ (𝑁 − 1))C(𝑁 − 1)) = (((𝑁↑2) + 𝑁) / 2)) |
| 45 | 12, 28, 44 | 3eqtrd 2781 |
. . 3
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ (1...𝑁)𝑘 = (((𝑁↑2) + 𝑁) / 2)) |
| 46 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑁 = 0 → (1...𝑁) = (1...0)) |
| 47 | | fz10 13585 |
. . . . . . 7
⊢ (1...0) =
∅ |
| 48 | 46, 47 | eqtrdi 2793 |
. . . . . 6
⊢ (𝑁 = 0 → (1...𝑁) = ∅) |
| 49 | 48 | sumeq1d 15736 |
. . . . 5
⊢ (𝑁 = 0 → Σ𝑘 ∈ (1...𝑁)𝑘 = Σ𝑘 ∈ ∅ 𝑘) |
| 50 | | sum0 15757 |
. . . . 5
⊢
Σ𝑘 ∈
∅ 𝑘 =
0 |
| 51 | 49, 50 | eqtrdi 2793 |
. . . 4
⊢ (𝑁 = 0 → Σ𝑘 ∈ (1...𝑁)𝑘 = 0) |
| 52 | | sq0i 14232 |
. . . . . . . 8
⊢ (𝑁 = 0 → (𝑁↑2) = 0) |
| 53 | | id 22 |
. . . . . . . 8
⊢ (𝑁 = 0 → 𝑁 = 0) |
| 54 | 52, 53 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑁 = 0 → ((𝑁↑2) + 𝑁) = (0 + 0)) |
| 55 | | 00id 11436 |
. . . . . . 7
⊢ (0 + 0) =
0 |
| 56 | 54, 55 | eqtrdi 2793 |
. . . . . 6
⊢ (𝑁 = 0 → ((𝑁↑2) + 𝑁) = 0) |
| 57 | 56 | oveq1d 7446 |
. . . . 5
⊢ (𝑁 = 0 → (((𝑁↑2) + 𝑁) / 2) = (0 / 2)) |
| 58 | | 2cn 12341 |
. . . . . 6
⊢ 2 ∈
ℂ |
| 59 | | 2ne0 12370 |
. . . . . 6
⊢ 2 ≠
0 |
| 60 | 58, 59 | div0i 12001 |
. . . . 5
⊢ (0 / 2) =
0 |
| 61 | 57, 60 | eqtrdi 2793 |
. . . 4
⊢ (𝑁 = 0 → (((𝑁↑2) + 𝑁) / 2) = 0) |
| 62 | 51, 61 | eqtr4d 2780 |
. . 3
⊢ (𝑁 = 0 → Σ𝑘 ∈ (1...𝑁)𝑘 = (((𝑁↑2) + 𝑁) / 2)) |
| 63 | 45, 62 | jaoi 858 |
. 2
⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) → Σ𝑘 ∈ (1...𝑁)𝑘 = (((𝑁↑2) + 𝑁) / 2)) |
| 64 | 1, 63 | sylbi 217 |
1
⊢ (𝑁 ∈ ℕ0
→ Σ𝑘 ∈
(1...𝑁)𝑘 = (((𝑁↑2) + 𝑁) / 2)) |